case inl
α : Type u_1
β : Type ?u.230776
γ : Type ?u.230779
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s

case inr
α : Type u_1
β : Type ?u.230776
γ : Type ?u.230779
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s
α : Type u_1
β : Type ?u.230776
γ : Type ?u.230779
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s
split_ifs with h
no goals
case inl
α : Type u_1
β : Type ?u.230776
γ : Type ?u.230779
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s
rw [filter_cons_of_pos _ h, singleton_add]
no goals
case inr
α : Type u_1
β : Type ?u.230776
γ : Type ?u.230779
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s
rw [filter_cons_of_neg _ h, zero_add]