fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
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
⊢ ((fun u => sqrt (x u)) u, semiAdjoint R (cderiv R (fun u => sqrt (x u)) u)) =
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26483
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
⊢ (sqrt (x u), fun y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((2 * sqrt (x u))⁻¹ * y)) =
    (sqrt (x u), fun dy => semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u))))