Theorem: SimpleGraph.Menger.bot_Separates_iff (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
h : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a b : V
ha : a ∈ A
hb : b ∈ B
p : Walk ⊥ a b
⊢ ∃ x ∈ X, x ∈ Walk.support { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.to_Walk
Tactic:
cases p with
| nil => exact ⟨a, by simpa using h <| mem_inter_of_mem ha hb⟩
| cons h' _ => cases h'
State after:
no goals

State before:
case nil
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
h : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a : V
ha : a ∈ A
hb : a ∈ B
⊢ ∃ x ∈ X, x ∈ Walk.support { a := a, b := a, ha := ha, hb := hb, to_Walk := Walk.nil }.to_Walk
Tactic:
exact ⟨a, by simpa using h <| mem_inter_of_mem ha hb⟩
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
h : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a : V
ha : a ∈ A
hb : a ∈ B
⊢ a ∈ X ∧ a ∈ Walk.support { a := a, b := a, ha := ha, hb := hb, to_Walk := Walk.nil }.to_Walk
Tactic:
simpa using h <| mem_inter_of_mem ha hb
State after:
no goals

State before:
case cons
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
h : A ∩ B ⊆ X
x✝ : AB_Walk ⊥ A B
a b : V
ha : a ∈ A
hb : b ∈ B
v✝ : V
h' : Adj ⊥ a v✝
p✝ : Walk ⊥ v✝ b
⊢ ∃ x ∈ X, x ∈ Walk.support { a := a, b := b, ha := ha, hb := hb, to_Walk := Walk.cons h' p✝ }.to_Walk
Tactic:
cases h'
State after:
no goals