Theorem: SimpleGraph.Menger.min_cut.symm (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 G A B = min_cut G B A
Tactic:
simp_rw [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
⊢ Nat.find (_ : ∃ n, is_cut_set_size G A B n) = Nat.find (_ : ∃ n, is_cut_set_size G B A n)

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
⊢ Nat.find (_ : ∃ n, is_cut_set_size G A B n) = Nat.find (_ : ∃ n, is_cut_set_size G B A n)
Tactic:
congr 1
State after:
case e_p
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 G A B = is_cut_set_size G B A

State before:
case e_p
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 G A B = is_cut_set_size G B A
Tactic:
ext n
State after:
case e_p.h.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
n : ℕ
⊢ is_cut_set_size G A B n ↔ is_cut_set_size G B A n

State before:
case e_p.h.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
n : ℕ
⊢ is_cut_set_size G A B n ↔ is_cut_set_size G B A n
Tactic:
constructor <;> exact λ ⟨X, h⟩ => ⟨X.symm, by simp [h]⟩
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
n : ℕ
x✝ : is_cut_set_size G B A n
X : Separator G B A
h : Separator.card X = n
⊢ Separator.card (Separator.symm X) = n
Tactic:
simp [h]
State after:
no goals