no goals
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v ⬝ᵥ w = x * vecHead w + v ⬝ᵥ vecTail w
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]