refine ⟨hE', fun j ↦ ?_, (lec_iff _ _).mpr (fun j ↦ ?_), fun hf ↦ ?_⟩
case intro
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
hE' : E w' = E (trunc w)
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
case intro.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
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ w' j ≤ E w'

case intro.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
hE' : E w' = E (trunc w)
j : Fin (Nat.succ n)
⊢ trunc w j ≤ w' j

case intro.refine_3
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
hE' : E w' = E (trunc w)
hf : trunc w = w'
⊢ False