Theorem: SimpleGraph.Menger.min_cut.inter_le_min_cut (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
⊢ card (A ∩ B) ≤ min_cut G A B
Tactic:
rw [min_cut, Nat.le_find_iff]
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
⊢ ∀ m < card (A ∩ B), ¬is_cut_set_size G A B m

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
⊢ ∀ m < card (A ∩ B), ¬is_cut_set_size G A B m
Tactic:
rintro n hn ⟨⟨X, h⟩, h'⟩
State after:
case intro.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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : Separator.card { val := X, property := h } = n
⊢ False

State before:
case intro.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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : Separator.card { val := X, property := h } = n
⊢ False
Tactic:
simp only [Separator.card] at h'
State after:
case intro.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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : card X = n
⊢ False

State before:
case intro.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
n : ℕ
hn : n < card (A ∩ B)
X : Finset V
h : Separates G A B X
h' : card X = n
⊢ False
Tactic:
linarith [card_le_card h.inter_subset]
State after:
no goals