case a
α : Type u_1
β : Type ?u.245010
γ : Type ?u.245013
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝¹ b a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ s \ {a} ↔ a✝ ∈ erase s a
α : Type u_1
β : Type ?u.245010
γ : Type ?u.245013
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ s \ {a} = erase s a
ext
no goals
case a
α : Type u_1
β : Type ?u.245010
γ : Type ?u.245013
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝¹ b a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ s \ {a} ↔ a✝ ∈ erase s a
rw [mem_erase, mem_sdiff, mem_singleton, and_comm]