Theorem: SimpleGraph.Menger.bot_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
⊢ min_cut ⊥ A B = card (A ∩ B)
Tactic:
refine le_antisymm ?_ min_cut.inter_le_min_cut
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
⊢ min_cut ⊥ A B ≤ card (A ∩ B)

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
⊢ min_cut ⊥ A B ≤ card (A ∩ B)
Tactic:
rw [min_cut, Nat.find_le_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 ⊥ 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 ⊥ A B m
Tactic:
refine ⟨(A ∩ B).card, le_rfl, ?_⟩
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
⊢ is_cut_set_size ⊥ A B (card (A ∩ B))

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
⊢ is_cut_set_size ⊥ A B (card (A ∩ B))
Tactic:
simpa only [is_cut_set_size] using ⟨⟨A ∩ B, bot_Separates_iff.mpr le_rfl⟩, rfl⟩
State after:
no goals