iterate rewrite [count_eq_card]
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ card { a // (p ∘ f) a } ≤ card { a // p a }