Theorem: Matrix.toList_length (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
n : ℕ
v : Fin n → α
⊢ (toList v).length = n
Tactic:
induction n <;> simp[*]
State after:
no goals