Theorem: Turanpartition.card_sdiff_insert (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (A \ insert v B) = card (A \ B) - 1
Tactic:
rw [sdiff_insert]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (erase (A \ B) v) = card (A \ B) - 1

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (erase (A \ B) v) = card (A \ B) - 1
Tactic:
exact card_erase_of_mem (mem_sdiff.mpr ⟨hvA, hvB⟩)
State after:
no goals