cases' le_or_lt (w j) w.E with h' h'
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ w j ≤ E w ∨ a j = 0
case e_f.h.inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : w j ≤ E w
⊢ w j ≤ E w ∨ a j = 0

case e_f.h.inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : E w < w j
⊢ w j ≤ E w ∨ a j = 0