Theorem: SimpleGraph.Menger.Separates.inter_subset (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 : Separates G A B X
⊢ A ∩ B ⊆ X
Tactic:
intro x h1
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
h : Separates G A B X
x : V
h1 : x ∈ A ∩ B
⊢ x ∈ X

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 : Separates G A B X
x : V
h1 : x ∈ A ∩ B
⊢ x ∈ X
Tactic:
rw [mem_inter] at h1
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
h : Separates G A B X
x : V
h1 : x ∈ A ∧ x ∈ B
⊢ x ∈ X

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 : Separates G A B X
x : V
h1 : x ∈ A ∧ x ∈ B
⊢ x ∈ X
Tactic:
simpa using h ⟨x, x, h1.1, h1.2, Walk.nil⟩
State after:
no goals