unfold fwdDeriv
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
⊢ (fwdDeriv R fun w => sqrt (x w)) = fun w dw =>
    let xdx := fwdDeriv R x w dw;
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
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
⊢ (fun x_1 dx => ((fun w => sqrt (x w)) x_1, cderiv R (fun w => sqrt (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))