have hn : w.sum = n := Nat.eq_of_le_of_lt_succ hsum hE
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
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
⊢ 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
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ w j = w1 n j