Theorem: Weight.sum_w1 (Weights/Degree1.lean)

State before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ Weight.sum (w1 n) = n
Tactic:
simp [w1, Weight.sum, Finset.sum_ite, Finset.filter_ne']
State after:
no goals