[GOAL]
α : Type v
inst✝ : Fintype α
⊢ Small.{w, v} α
[PROOFSTEP]
rw [small_congr (Fintype.equivFin α)]
[GOAL]
α : Type v
inst✝ : Fintype α
⊢ Small.{w, 0} (Fin (Fintype.card α))
[PROOFSTEP]
infer_instance
