Theorem: SimpleGraph.Menger.AB_Walk.tototo (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 : V
hA : x ∈ A
hB : x ∈ B
⊢ False
Tactic:
cases h ▸ Finset.mem_inter.mpr ⟨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 : ∀ x ∈ A, x ∉ B
⊢ A ∩ B = ∅
Tactic:
ext x
State after:
case 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
h : ∀ x ∈ A, x ∉ B
x : V
⊢ x ∈ A ∩ B ↔ x ∈ ∅

State before:
case 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
h : ∀ x ∈ A, x ∉ B
x : V
⊢ x ∈ A ∩ B ↔ x ∈ ∅
Tactic:
constructor <;> intro h'
State after:
case a.mp
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 : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
⊢ x ∈ ∅

case a.mpr
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 : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ ∅
⊢ x ∈ A ∩ B

State before:
case a.mp
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 : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
⊢ x ∈ ∅
Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_inter.mp h'
State after:
case a.mp.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
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
h1 : x ∈ A
h2 : x ∈ B
⊢ x ∈ ∅

State before:
case a.mp.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
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
h1 : x ∈ A
h2 : x ∈ B
⊢ x ∈ ∅
Tactic:
cases h x h1 h2
State after:
no goals

State before:
case a.mpr
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 : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ ∅
⊢ x ∈ A ∩ B
Tactic:
cases h'
State after:
no goals