Theorem: Weight.pair_shift (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ pair (k • 1) ↑a = k * d
Tactic:
simp only [pair, smul_apply, one_apply, mul_one]
State after:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), ↑a x * k = k * d

State before:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), ↑a x * k = k * d
Tactic:
rw [mul_comm k, ← Finset.sum_mul]
State after:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ (∑ i : Fin (Nat.succ n), ↑a i) * k = d * k