case a
α : Type u_1
β : Type ?u.390807
γ : Type ?u.390810
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (erase s a) ↔ x ∈ erase (filter p s) a
α : Type u_1
β : Type ?u.390807
γ : Type ?u.390810
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (erase s a) = erase (filter p s) a
ext x
no goals
case a
α : Type u_1
β : Type ?u.390807
γ : Type ?u.390810
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (erase s a) ↔ x ∈ erase (filter p s) a
simp only [and_assoc, mem_filter, iff_self_iff, mem_erase]