Theorem: SciLean.Scalar.sqrt.arg_x.cderiv_rule (SciLean/Core/Functions/Pow.lean)

State before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x : W → R
hx : CDifferentiable R x
hw : ∀ (w : W), 0 < x w
⊢ (cderiv R fun w => sqrt (x w)) = fun w dw =>
    let xdx := fwdDeriv R x w dw;
    xdx.2 / (2 * sqrt xdx.1)
Tactic:
funext x
State after:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x : W
⊢ cderiv R (fun w => sqrt (x✝ w)) x = fun dw =>
    let xdx := fwdDeriv R x✝ x dw;
    xdx.2 / (2 * sqrt xdx.1)

State before:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x : W
⊢ cderiv R (fun w => sqrt (x✝ w)) x = fun dw =>
    let xdx := fwdDeriv R x✝ x dw;
    xdx.2 / (2 * sqrt xdx.1)
Tactic:
fun_trans (disch:=aesop)
State after:
no goals

State before:
case funProp.discharger
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.3755
inst✝ : SemiInnerProductSpace R U
x✝ : W → R
hx : CDifferentiable R x✝
hw : ∀ (w : W), 0 < x✝ w
x : W
⊢ 0 < x✝ x
Tactic:
aesop
State after:
no goals