no goals
α : Type u_1
β : Type ?u.268298
γ : Type ?u.268301
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a => p a ∨ q a) s + filter (fun a => p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun a => p a ∨ q a) (a ::ₘ s) + filter (fun a => p a ∧ q a) (a ::ₘ s)
by_cases p a <;> by_cases q a <;> simp [*]