rw [mem_sdiff] at *
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A \ insert v B
⊢ a✝ ≠ v ∧ a✝ ∈ A \ B
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ ¬a✝ ∈ insert v B
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B