refine ⟨fun h ↦ (lec_iff _ _).mpr (fun j ↦ ?_), dom_of_gec hE⟩
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
⊢ w ≤ w' ↔ w' ≤ w
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw₁ : w 0 = 0
hw'₂ : balanced w'
hE : E w = E w'
h : w ≤ w'
j : Fin (Nat.succ n)
⊢ w' j ≤ w j