internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
z : V
hz1 : z ∈ ↑Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
this : z ∈ List.map (merge_edge e) (Walk.support p.to_Walk)
⊢ z ∈ Walk.support p.to_Walk
Tactic:
simp at this
Proof state after:
case mk.refine_1.h.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
z : V
hz1 : z ∈ ↑Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
this : ∃ a ∈ Walk.support p.to_Walk, merge_edge e a = z
⊢ z ∈ Walk.support p.to_Walk
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
z : V
hz1 : z ∈ ↑Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
this : ∃ a ∈ Walk.support p.to_Walk, merge_edge e a = z
⊢ z ∈ Walk.support p.to_Walk
Tactic:
obtain ⟨a, ha1, ha2⟩ := this
Proof state after:
case mk.refine_1.h.intro.intro.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
z : V
hz1 : z ∈ ↑Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
a : V
ha1 : a ∈ Walk.support p.to_Walk
ha2 : merge_edge e a = z
⊢ z ∈ Walk.support p.to_Walk
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h.intro.intro.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
z : V
hz1 : z ∈ ↑Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
a : V
ha1 : a ∈ Walk.support p.to_Walk
ha2 : merge_edge e a = z
⊢ z ∈ Walk.support p.to_Walk
Tactic:
by_cases h : a = e.snd <;> simp [merge_edge, update, h] at ha2 <;> subst_vars
Proof state after:
case pos
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
hz1 : e.toProd.1 ∈ ↑Y
hz2 : e.toProd.1 ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
ha1 : e.toProd.2 ∈ Walk.support p.to_Walk
⊢ e.toProd.1 ∈ Walk.support p.to_Walk

case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
a : V
ha1 : a ∈ Walk.support p.to_Walk
h : ¬a = e.toProd.2
hz1 : a ∈ ↑Y
hz2 : a ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
⊢ a ∈ Walk.support p.to_Walk
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case pos
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
hz1 : e.toProd.1 ∈ ↑Y
hz2 : e.toProd.1 ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
ha1 : e.toProd.2 ∈ Walk.support p.to_Walk
⊢ e.toProd.1 ∈ Walk.support p.to_Walk
Tactic:
contradiction
Proof state after:
no goals
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case neg
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
x✝ : e.toProd.1 ∉ ↑Y
p : AB_Walk G A B
a : V
ha1 : a ∈ Walk.support p.to_Walk
h : ¬a = e.toProd.2
hz1 : a ∈ ↑Y
hz2 : a ∈ Walk.support (push_Walk (merge_edge e) p.to_Walk)
⊢ a ∈ Walk.support p.to_Walk
Tactic:
assumption
Proof state after:
no goals
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_2
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
⊢ e.toProd.2 ∈ X
Tactic:
simp [mem_union, mem_singleton]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_3
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
⊢ card X = min_cut G A B
Tactic:
refine le_antisymm ?_ (min_cut.le' X_sep_AB)
Proof state after:
case mk.refine_3
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
⊢ card X ≤ min_cut G A B
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_3
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X✝ Y✝ Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
A₁ : Finset V := image (merge_edge e) A
B₁ : Finset V := image (merge_edge e) B
Y : Separator (G /ₑ e) A₁ B₁
Y_eq_min₁ : Separator.card Y = min_cut (G /ₑ e) A₁ B₁
X : Finset V := ↑Y ∪ {e.toProd.2}
Y_lt_min : Separator.card Y < min_cut G A B
X_sep_AB : Separates G A B X
⊢ card X ≤ min_cut G A B
Tactic:
exact (card_union_le _ _).trans (Nat.succ_le_of_lt Y_lt_min)
Proof state after:
no goals
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
e : Dart G
⊢ isMenger (G /ₑ e) → isMenger (G -ₑ Dart.edge e) → isMenger G
Tactic:
intro h_contract h_minus A B
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
apply not_imp_self.mp
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
⊢ (¬∃ P, pwd P ∧ card P = min_cut G A B) → ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
⊢ (¬∃ P, pwd P ∧ card P = min_cut G A B) → ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
intro too_small
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ¬∃ P, pwd P ∧ card P = min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ¬∃ P, pwd P ∧ card P = min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
push_neg at too_small
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P ≠ min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P ≠ min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
replace too_small : ∀ P : Finset (AB_Walk G A B), pwd P → P.card < min_cut G A B
Proof state after:
case too_small
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P ≠ min_cut G A B
⊢ ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B

V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
obtain ⟨X, ex_in_X, ey_in_X, X_sep_AB, X_eq_min⟩ := step_1 h_contract too_small
Proof state after:
case intro.intro.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case intro.intro.intro.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
obtain ⟨P, hP⟩ := sep_cleanup ex_in_X ey_in_X X_eq_min X_sep_AB (h_minus A X)
Proof state after:
case intro.intro.intro.intro.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case intro.intro.intro.intro.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
have X_eq_min' : X.card = min_cut G B A := X_eq_min.trans min_cut.symm
Proof state after:
case intro.intro.intro.intro.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case intro.intro.intro.intro.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
obtain ⟨Q, hQ⟩ := sep_cleanup ex_in_X ey_in_X X_eq_min' X_sep_AB.symm (h_minus B X)
Proof state after:
case intro.intro.intro.intro.mk.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
Q : Finset (AB_Walk G B X)
hQ : pwd Q ∧ card Q = card X ∧ ∀ (p : { x // x ∈ Q }), minimal ↑p
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case intro.intro.intro.intro.mk.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
Q : Finset (AB_Walk G B X)
hQ : pwd Q ∧ card Q = card X ∧ ∀ (p : { x // x ∈ Q }), minimal ↑p
⊢ ∃ P, pwd P ∧ card P = min_cut G A B
Tactic:
rw [← X_eq_min]
Proof state after:
case intro.intro.intro.intro.mk.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
Q : Finset (AB_Walk G B X)
hQ : pwd Q ∧ card Q = card X ∧ ∀ (p : { x // x ∈ Q }), minimal ↑p
⊢ ∃ P, pwd P ∧ card P = card X
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case intro.intro.intro.intro.mk.mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
Q : Finset (AB_Walk G B X)
hQ : pwd Q ∧ card Q = card X ∧ ∀ (p : { x // x ∈ Q }), minimal ↑p
⊢ ∃ P, pwd P ∧ card P = card X
Tactic:
apply Subtype.exists_of_subtype
Proof state after:
case intro.intro.intro.intro.mk.mk.a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
Q : Finset (AB_Walk G B X)
hQ : pwd Q ∧ card Q = card X ∧ ∀ (p : { x // x ∈ Q }), minimal ↑p
⊢ { x // pwd x ∧ card x = card X }
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case intro.intro.intro.intro.mk.mk.a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X✝ Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
X : Finset V
ex_in_X : e.toProd.1 ∈ X
ey_in_X : e.toProd.2 ∈ X
X_sep_AB : Separates G A B X
X_eq_min : card X = min_cut G A B
P : Finset (AB_Walk G A X)
hP : pwd P ∧ card P = card X ∧ ∀ (p : { x // x ∈ P }), minimal ↑p
X_eq_min' : card X = min_cut G B A
Q : Finset (AB_Walk G B X)
hQ : pwd Q ∧ card Q = card X ∧ ∀ (p : { x // x ∈ Q }), minimal ↑p
⊢ { x // pwd x ∧ card x = card X }
Tactic:
exact stitch X_sep_AB P hP.1 hP.2.1 Q hQ.1 hQ.2.1 hP.2.2 hQ.2.2
Proof state after:
no goals
Theorem: SimpleGraph.Menger.induction_step
Proof state before:
case too_small
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A✝ B✝ X Y Z : Finset V
e : Dart G
h_contract : isMenger (G /ₑ e)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
too_small : ∀ (P : Finset (AB_Walk G A B)), pwd P → card P ≠ min_cut G A B
⊢ ∀ (P : Finset (AB_Walk G A B)), pwd P → card P < min_cut G A B
Tactic:
exact λ P h => lt_of_le_of_ne (upper_bound h) (too_small P h)
Proof state after:
no goals
Theorem: SimpleGraph.Menger.Menger
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
⊢ isMenger G
Tactic:
induction' h : Fintype.card G.edgeSet using Nat.strongInductionOn with n ih generalizing G
Proof state after:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
n : ℕ
ih : ∀ m < n, ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
G : SimpleGraph V
h : Fintype.card ↑(edgeSet G) = n
⊢ isMenger G
Theorem: SimpleGraph.Menger.Menger
Proof state before:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
n : ℕ
ih : ∀ m < n, ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
G : SimpleGraph V
h : Fintype.card ↑(edgeSet G) = n
⊢ isMenger G
Tactic:
subst h
Proof state after:
case ind
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
G : SimpleGraph V
ih : ∀ m < Fintype.card ↑(edgeSet G), ∀ {G : SimpleGraph V}, Fintype.card ↑(edgeSet G) = m → isMenger G
⊢ isMenger G