refine hne <| lec_antisymm hc <|
  (dom_iff_gec_of_balanced (trunc_normalized hw).1 hb' hE'.symm).mp <|
  w.trunc_dom.trans <| hmin _ ?_ <| (dom_of_gec hE' hc).trans w.trunc_dom
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ False
case intro.intro.intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
⊢ Monotone (Function.update (trunc w) k 1)