rewrite [count_eq_card]
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ card { a // p a } = count (p ∘ Subtype.val)
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ card { a // p a } = card { a // (p ∘ Subtype.val) a }