fun_prop (disch:=aesop)
case left
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ CDifferentiableAt R (fun u => sqrt (x u)) u

case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R (cderiv R (fun u => sqrt (x u)) u)
case right
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.17689
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : 0 < x u
⊢ HasSemiAdjoint R (cderiv R (fun u => sqrt (x u)) u)