Theorem: SimpleGraph.Menger.upper_bound (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
P : Finset (AB_Walk G A B)
dis : pwd P
⊢ card P ≤ min_cut G A B
Tactic:
obtain ⟨⟨X, h₁⟩, h₂⟩ := min_cut.set G A B
State after:
case 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
P : Finset (AB_Walk G A B)
dis : pwd P
X : Finset V
h₁ : Separates G A B X
h₂ : Separator.card { val := X, property := h₁ } = min_cut G A B
⊢ card P ≤ min_cut G A B

State before:
case 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
P : Finset (AB_Walk G A B)
dis : pwd P
X : Finset V
h₁ : Separates G A B X
h₂ : Separator.card { val := X, property := h₁ } = min_cut G A B
⊢ card P ≤ min_cut G A B
Tactic:
simpa [← h₂] using path_le_cut dis h₁
State after:
no goals