rw [sdiff_erase hB hv]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
hv2 : ¬v ∈ A \ B
⊢ card (A \ erase B v) = card (A \ B) + 1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
hv2 : ¬v ∈ A \ B
⊢ card (A \ B ∪ {v}) = card (A \ B) + 1