simp only [Finset.mem_univ, not_true, ge_iff_le, zero_le, min_eq_left, add_zero]
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)
no goals