Theorem: LeanColls.IndexType.length_toList_univ (LeanColls/Classes/IndexType/Basic.lean)

State before:
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (toList (univ α)).length = card α
Tactic:
rw [LawfulIndexType.toList_eq_ofFn]
State after:
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (List.ofFn fromFin).length = card α

State before:
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (List.ofFn fromFin).length = card α
Tactic:
simp
State after:
no goals