no goals
α : Type u_1
β : Type ?u.59235
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : card s = n + 1
a : α
has : a ∈ s
⊢ card (erase s a) = n
simp only [h, card_erase_of_mem has, add_tsub_cancel_right]