case a
α : Type u_1
β : Type ?u.379119
γ : Type ?u.379122
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (insert a s) ↔ x ∈ if p a then insert a (filter p s) else filter p s
α : Type u_1
β : Type ?u.379119
γ : Type ?u.379122
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (insert a s) = if p a then insert a (filter p s) else filter p s
ext x
no goals
case a
α : Type u_1
β : Type ?u.379119
γ : Type ?u.379122
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (insert a s) ↔ x ∈ if p a then insert a (filter p s) else filter p s
split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']