Theorem: SimpleGraph.Menger.induction_step (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
⊢ isMenger (G /ₑ e) → isMenger (G -ₑ Dart.edge e) → isMenger G
Tactic:
intro h_contract h_minus A 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)
h_minus : isMenger (G -ₑ Dart.edge e)
A B : Finset V
⊢ ∃ P, pwd P ∧ card P = 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)
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
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

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

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

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

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

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

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

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

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

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

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

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