exact this
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
no goals