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