assumption
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.13231
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x dx : W
⊢ ∀ (w : W), 0 < x✝ w
no goals