internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case 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)
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, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
have X_sep_AB : Separates G A B X := sep_of_sep_in_merge Y.prop
Proof state after:
case 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)
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 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case 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)
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 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
refine ⟨X, ?_, ?_, X_sep_AB, ?_⟩
Proof state after:
case mk.refine_1
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.1 ∈ X

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

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:
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}
⊢ Separator.card Y < min_cut G A B
Tactic:
obtain ⟨P₁, P₁_dis, P₁_eq_min₁⟩ := h_contract A₁ B₁
Proof state after:
case 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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ Separator.card Y < min_cut G A B
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case 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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ Separator.card Y < min_cut G A B
Tactic:
rw [Y_eq_min₁, ← P₁_eq_min₁]
Proof state after:
case 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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ card P₁ < min_cut G A B
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case 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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ card P₁ < min_cut G A B
Tactic:
rw [← card_image_of_injective P₁ AB_Walk.lift_inj]
Proof state after:
case 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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ card (image (lift (merge_edge e) ?m.673897) 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)
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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ Adapted G (merge_edge e)
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case 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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ card (image (lift (merge_edge e) ?m.673897) P₁) < min_cut G A B
Tactic:
apply too_small
Proof state after:
case intro.intro.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)
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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ pwd (image (lift (merge_edge e) ?m.673897) P₁)
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case intro.intro.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)
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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ pwd (image (lift (merge_edge e) ?m.673897) P₁)
Tactic:
apply AB_lift_dis
Proof state after:
case intro.intro.a.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)
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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ pwd P₁
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case intro.intro.a.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)
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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ pwd P₁
Tactic:
exact P₁_dis
Proof state after:
no goals
Theorem: SimpleGraph.Menger.step_1
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)
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}
P₁ : Finset (AB_Walk (G /ₑ e) A₁ B₁)
P₁_dis : pwd P₁
P₁_eq_min₁ : card P₁ = min_cut (G /ₑ e) A₁ B₁
⊢ Adapted G (merge_edge e)
Tactic:
exact merge_edge_adapted
Proof state after:
no goals
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1
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.1 ∈ X
Tactic:
rw [mem_union]
Proof state after:
case mk.refine_1
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.1 ∈ ↑Y ∨ e.toProd.1 ∈ {e.toProd.2}
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1
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.1 ∈ ↑Y ∨ e.toProd.1 ∈ {e.toProd.2}
Tactic:
left
Proof state after:
case mk.refine_1.h
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.1 ∈ ↑Y
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h
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.1 ∈ ↑Y
Tactic:
by_contra
Proof state after:
case mk.refine_1.h
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
⊢ False
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h
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
⊢ False
Tactic:
suffices Separates G A B Y.val from not_lt_of_le (min_cut.le' this) Y_lt_min
Proof state after:
case mk.refine_1.h
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
⊢ Separates G A B ↑Y
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h
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
⊢ Separates G A B ↑Y
Tactic:
intro p
Proof state after:
case mk.refine_1.h
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
⊢ ∃ x ∈ ↑Y, x ∈ Walk.support p.to_Walk
Theorem: SimpleGraph.Menger.step_1
Proof state before:
case mk.refine_1.h
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
⊢ ∃ x ∈ ↑Y, x ∈ Walk.support p.to_Walk
Tactic:
obtain ⟨z, hz1, hz2⟩ := Y.prop (p.push <| merge_edge e)
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 (merge_edge e) p).to_Walk
⊢ ∃ x ∈ ↑Y, x ∈ 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 (merge_edge e) p).to_Walk
⊢ ∃ x ∈ ↑Y, x ∈ Walk.support p.to_Walk
Tactic:
refine ⟨z, hz1, ?_⟩
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 (merge_edge e) p).to_Walk
⊢ 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 (merge_edge e) p).to_Walk
⊢ z ∈ Walk.support p.to_Walk
Tactic:
simp [push, push_Walk] at hz2
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)
⊢ 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)
⊢ z ∈ Walk.support p.to_Walk
Tactic:
have := support_push_Walk hz2
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 : z ∈ List.map (merge_edge e) (Walk.support p.to_Walk)
⊢ z ∈ Walk.support p.to_Walk