have hc₁ := (lec_iff _ _).mp
              ((dom_iff_gec_of_balanced hw (w1_balanced n) (hE.trans (E_w1 n).symm)).mp h₂)
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
⊢ w j = w1 n j
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
⊢ w j = w1 n j