rw [← Finset.sum_erase_add _ _ (Finset.mem_univ k), add_comm, add_left_inj, hk]
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
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
⊢ ∑ x in Finset.erase Finset.univ k, min (w x) (E w) = ∑ x in Finset.erase Finset.univ k, min (w x) (E w) + min 0 (E w)