case a
α : Type u_1
β : Type ?u.12293
γ : Type ?u.12296
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a sᶜ ↔ a✝ ∈ erase (sᶜ) a
α : Type u_1
β : Type ?u.12293
γ : Type ?u.12296
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a : α
⊢ insert a sᶜ = erase (sᶜ) a
ext
no goals
case a
α : Type u_1
β : Type ?u.12293
γ : Type ?u.12296
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a sᶜ ↔ a✝ ∈ erase (sᶜ) a
simp only [not_or, mem_insert, iff_self_iff, mem_compl, mem_erase]