ext j
case e_f
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ (fun x => a x * min (w x) (E w)) = fun j => a j * w j
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)
⊢ a j * min (w j) (E w) = a j * w j