no goals
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ a₂ : α
⊢ x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]
rw [smul_cons, smul_cons, smul_cons, smul_empty]