Theorem: SimpleGraph.Menger.Separator.card_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
X : Separator G A B
⊢ card (symm X) = card X
Tactic:
cases X
State after:
case 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 val✝ : Finset V
property✝ : Separates G A B val✝
⊢ card (symm { val := val✝, property := property✝ }) = card { val := val✝, property := property✝ }

State before:
case 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 val✝ : Finset V
property✝ : Separates G A B val✝
⊢ card (symm { val := val✝, property := property✝ }) = card { val := val✝, property := property✝ }
Tactic:
simp [symm, card]
State after:
no goals