assumption
case funProp.discharger
R✝ : Type ?u.13993
C : Type ?u.13992
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.14002
inst✝⁴ : Vec C W✝
U✝ : Type ?u.14025
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.14075
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : x w ≠ 0
dx : W
⊢ x w ≠ 0
no goals