refine le_antisymm ?_ (le_of_eq_of_le hE.symm ?_) <;> rw [E, add_le_add_iff_right]
case hE'
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
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) + 1 = E w
case hE'.refine_1
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
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ (Weight.sum (trunc w) + 1) * d / (n + 1) ≤ Weight.sum w * d / (n + 1)

case hE'.refine_2
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
hsum' : Weight.sum w' = Weight.sum (trunc w) + 1
⊢ Weight.sum (trunc w) * d / (n + 1) ≤ (Weight.sum (trunc w) + 1) * d / (n + 1)