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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ E (w + k • 1) = E w + k * d
Tactic:
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]
State after:
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

State before:
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
Tactic:
rw [add_mul, mul_assoc, Nat.add_mul_div_left _ _ (Nat.succ_pos n)]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x) * d / Nat.succ n + k * d + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x) * d / Nat.succ n + k * d + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d
Tactic:
abel
State after:
no goals