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