case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.327024
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countp p (map f 0) = ↑card (filter (fun a => p (f a)) 0)

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.327024
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countp p (map f t) = ↑card (filter (fun a => p (f a)) t)
⊢ countp p (map f (a ::ₘ t)) = ↑card (filter (fun a => p (f a)) (a ::ₘ t))
α : Type u_1
β : Type u_2
γ : Type ?u.327024
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countp p (map f s) = ↑card (filter (fun a => p (f a)) s)
refine' Multiset.induction_on s _ fun a t IH => _
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.327024
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countp p (map f 0) = ↑card (filter (fun a => p (f a)) 0)
rw [map_zero, countp_zero, filter_zero, card_zero]
no goals
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.327024
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countp p (map f t) = ↑card (filter (fun a => p (f a)) t)
⊢ countp p (map f (a ::ₘ t)) = ↑card (filter (fun a => p (f a)) (a ::ₘ t))
rw [map_cons, countp_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
  add_comm]