Theorem: LeanColls.Seq.size_ofFn (LeanColls/Classes/Seq.lean)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
⊢ size (ofFn f) = n
Tactic:
simp [size_def, toList_ofFn, List.instSeqList]
State after:
no goals