simp only [E, Weight.sum, Nat.succ_eq_add_one, add_apply, smul_apply, one_apply, mul_one,
  Finset.sum_add_distrib, Finset.sum_const, Finset.card_fin, smul_eq_mul]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ E (w + k • 1) = E w + k * d
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x + (n + 1) * k) * d / (n + 1) + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d