α : Type u_1
β : Type ?u.208349
γ : Type ?u.208352
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hs : b ∈ s
hsa : b ≠ a → ¬b ∈ s
⊢ b = a
α : Type u_1
β : Type ?u.208349
γ : Type ?u.208352
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hs : b ∈ s
hsa : ¬b ∈ erase s a
⊢ b = a
rw [mem_erase, not_and] at hsa
no goals
α : Type u_1
β : Type ?u.208349
γ : Type ?u.208352
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hs : b ∈ s
hsa : b ≠ a → ¬b ∈ s
⊢ b = a
exact not_imp_not.mp hsa hs