feat(combinatorics\quiver\max_flow_mion_cut)

leanprover-community · Mar 20, 2023 · 6661c3e · 6661c3e
1 parent accc92c
commit 6661c3e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/leanpkg.toml b/leanpkg.toml
@@ -5,3 +5,4 @@ lean_version = "leanprover-community/lean:3.50.3"
 path = "src"
 
 [dependencies]
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "290a7ba01fbcab1b64757bdaa270d28f4dcede35"}
diff --git a/src/combinatorics/quiver/max_flow_min_cut.lean b/src/combinatorics/quiver/max_flow_min_cut.lean
@@ -460,7 +460,12 @@ begin
     simp,
     unfold mk_in,
     have nonneg_flow: ∀ v ∈ V', ∀ u ∈ S, afn.f u v ≥ 0 :=
-    by {intros v vInV' u uInS, exact afn.non_neg_flow u v}, -- meta errors again?
+    begin
+      intros v vInV' u uInS,
+      have h1: v ∈ V' := by {exact vInV'},
+      have h2: u ∈ S := by {exact uInS},
+      exact afn.non_neg_flow u v,
+    end,
     exact finset.sum_nonneg nonneg_flow,
   end,
   apply le_trans lemma3 lemma2,
Original file line number	Diff line number	Diff line change
Expand Up		@@ -5,3 +5,4 @@ lean_version = "leanprover-community/lean:3.50.3"
		path = "src"

		[dependencies]
		mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "290a7ba01fbcab1b64757bdaa270d28f4dcede35"}