simp only [f, pair, ge_iff_le, tsub_le_iff_right, Nat.sub_sub]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : Fin (Nat.succ n)
⊢ f w (tw n d k) = E w - (d - 1) * w 0 - w k
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : Fin (Nat.succ n)
⊢ E w - ∑ j : Fin (Nat.succ n), ↑(tw n d k) j * w j = E w - ((d - 1) * w 0 + w k)