case h.e'_2
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = Finset.card Finset.univ
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = n
convert Finset.card_fin n
no goals
case h.e'_2
n : ℕ
⊢ Fintype.card ↑(incl.obj (mk n)) = Finset.card Finset.univ
apply Fintype.ofEquiv_card