simp only [Weight.sum, ne_eq, Function.update_apply, trunc_apply, ge_iff_le, Finset.sum_ite,
  Finset.mem_univ, forall_true_left, Finset.filter_eq', ite_true, Finset.sum_const,
  Finset.card_singleton, smul_eq_mul, mul_one, forall_eq, Finset.filter_ne', not_true]
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ Weight.sum w' = Weight.sum (trunc w) + 1
case hsum'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
j : Fin (Nat.succ n)
hj : E w < w j
⊢ 1 + ∑ x in Finset.erase Finset.univ k, min (w x) (E w) = ∑ x : Fin (Nat.succ n), min (w x) (E w) + 1