Theorem: SimpleGraph.Menger.sep_of_sep_in_merge (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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
⊢ Separates G A B (Y ∪ {e.toProd.2})
Tactic:
rintro γ
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk

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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨z, hz1, hz2⟩ := Y_sep (γ.push (merge_edge e))
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push (merge_edge e) γ).to_Walk
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk

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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push (merge_edge e) γ).to_Walk
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
simp [mem_inter, push] at hz2
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk

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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
have := support_push_Walk hz2
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : z ∈ List.map (merge_edge e) (Walk.support γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk

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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : z ∈ List.map (merge_edge e) (Walk.support γ.to_Walk)
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
simp at this
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : ∃ a ∈ Walk.support γ.to_Walk, merge_edge e a = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk

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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
this : ∃ a ∈ Walk.support γ.to_Walk, merge_edge e a = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
obtain ⟨x, hx₁, hx₂⟩ := this
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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk

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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ ∃ x ∈ Y ∪ {e.toProd.2}, x ∈ Walk.support γ.to_Walk
Tactic:
use x
State after:
case 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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ x ∈ Y ∪ {e.toProd.2} ∧ x ∈ Walk.support γ.to_Walk

State before:
case 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
Y_sep : Separates (G /ₑ e) (image (merge_edge e) A) (image (merge_edge e) B) Y
γ : AB_Walk G A B
z : V
hz1 : z ∈ Y
hz2 : z ∈ Walk.support (push_Walk (merge_edge e) γ.to_Walk)
x : V
hx₁ : x ∈ Walk.support γ.to_Walk
hx₂ : merge_edge e x = z
⊢ x ∈ Y ∪ {e.toProd.2} ∧ x ∈ Walk.support γ.to_Walk
Tactic:
by_cases h : x = e.snd <;> simp [merge_edge, update, h] at hx₂ <;> subst_vars <;> simp [hx₁, hz1]
State after:
no goals