Theorem: SimpleGraph.Menger.step_1 (Untitled/Graphs/Menger.lean)

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
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
let A₁ := image (merge_edge e) A
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)
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
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B

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
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
let B₁ := image (merge_edge e) B
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)
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
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B

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
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
obtain ⟨Y, Y_eq_min₁⟩ := min_cut.set (G /ₑ e) A₁ B₁
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, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B

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, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B
Tactic:
let X := Y.val ∪ {e.snd}
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}
⊢ ∃ X, e.toProd.1 ∈ X ∧ e.toProd.2 ∈ X ∧ Separates G A B X ∧ card X = min_cut G A B

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
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

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, ?_⟩
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

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₁
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

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₁]
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

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]
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)

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
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₁)

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
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₁

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
State after:
no goals

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
State after:
no goals

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]
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}

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
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

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
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

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
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

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
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

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)
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

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, ?_⟩
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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)
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

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)
State after:
no goals