Theorem: Weight.pair'_v (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ pair' w (v a) = ↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)
Tactic:
simp [v, pair, pair', Weight.sum, Finset.mul_sum, Finset.sum_sub_distrib, sub_mul, mul_assoc]
State after:
no goals