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

State before:
n d : ℕ
inst✝ : NeZero d
w w' a : Weight n d
⊢ pair (w + w') a = pair w a + pair w' a
Tactic:
simp only [pair, add_apply, mul_add, Finset.sum_add_distrib]
State after:
no goals