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

State before:
α : Type u_1
n : ℕ
v : Fin n → α
⊢ (toOptionVec fun i => some (v i)) = some v
Tactic:
induction n <;> simp[*, Matrix.empty_eq, toOptionVec, Function.comp]
State after:
no goals