cases h with
| inl h =>  exact ⟨h.1, fun _ => h.2⟩;
| inr h => 
  by_contra h'; push_neg at h' 
  have ha := hB hv
  have := mem_singleton.mp h; rw [← this] at ha 
  exact (h' ha).1 this
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 ∧ ¬a ∈ B ∨ a ∈ {v}
⊢ a ∈ A ∧ (a ≠ v → ¬a ∈ B)
no goals