no goals
α : Type u_1
β : Type ?u.231954
γ : Type ?u.231957
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
a : α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅
simp only [singleton, filter_cons, filter_zero, add_zero, empty_eq_zero]