no goals
α✝ : Type u_1
p q : α✝ → Bool
a : α✝
l : List α✝
⊢ filter p (filter q (a :: l)) = filter (fun a => decide (p a = true ∧ q a = true)) (a :: l)
by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]