simp only [pair, tw, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply, mul_ite,
  mul_one, mul_zero, add_mul, ite_mul, zero_mul, one_mul, Finset.sum_add_distrib,
  Finset.sum_ite_eq', Finset.mem_univ, ite_true]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : Fin (Nat.succ n)
⊢ pair w ↑(tw n d k) = (d - 1) * w 0 + w k
no goals