α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑card (filter (fun x => True = p x) s) = ↑card (filter p s)
α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ count True (map p s) = ↑card (filter p s)
simp only [count_eq_card_filter_eq, map_filter, card_map, Function.comp.left_id,
  eq_true_eq_id, Function.comp]
case h.e_6.h.e_p
α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (fun x => True = p x) = p
α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑card (filter (fun x => True = p x) s) = ↑card (filter p s)
congr
case h.e_6.h.e_p.h
α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
x✝ : α
⊢ (True = p x✝) = p x✝
case h.e_6.h.e_p
α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (fun x => True = p x) = p
funext _
no goals
case h.e_6.h.e_p.h
α : Type u_1
β : Type ?u.434603
γ : Type ?u.434606
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
x✝ : α
⊢ (True = p x✝) = p x✝
simp only [eq_iff_iff, true_iff]