no goals
l m✝ n : ℕ
α : Type u_1
β : Type ?u.26440
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b
simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
    Function.comp_apply]