simp_rw [pair, smul_apply, mul_left_comm]
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ pair (k • w) a = k * pair w a
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), k * (a x * w x) = k * ∑ j : Fin (Nat.succ n), a j * w j