rw [mem_sdiff]
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A \ erase B v
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A ∧ ¬a ∈ erase B v