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

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