rw [mem_erase] at h
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ erase (A \ B) v
⊢ a✝ ∈ A \ insert v B
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A \ insert v B