case inl
α : Type u_1
β : Type ?u.397803
γ : Type ?u.397806
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

case inr
α : Type u_1
β : Type ?u.397803
γ : Type ?u.397806
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0
α : Type u_1
β : Type ?u.397803
γ : Type ?u.397806
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0
split_ifs with h
no goals
case inl
α : Type u_1
β : Type ?u.397803
γ : Type ?u.397806
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s
exact count_filter_of_pos h
no goals
case inr
α : Type u_1
β : Type ?u.397803
γ : Type ?u.397806
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0
exact count_filter_of_neg h