Theorem: SciLean.Scalar.sqrt.arg_x.fwdDeriv_rule_at (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.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
⊢ fwdDeriv R (fun w => sqrt (x w)) w = fun dw =>
    let xdx := fwdDeriv R x w dw;
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Tactic:
unfold fwdDeriv
State after:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
⊢ (fun dx => ((fun w => sqrt (x w)) w, cderiv R (fun w => sqrt (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))

State before:
R : Type u_1
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type ?u.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
⊢ (fun dx => ((fun w => sqrt (x w)) w, cderiv R (fun w => sqrt (x w)) w dx)) = fun dw =>
    let xdx := (x w, cderiv R x w dw);
    let x' := sqrt xdx.1;
    (x', xdx.2 / (2 * x'))
Tactic:
fun_trans (disch:=assumption) [fwdDeriv]
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.8937
inst✝ : SemiInnerProductSpace R U
w : W
x : W → R
hx : CDifferentiableAt R x w
hw : 0 < x w
dx : W
⊢ 0 < x w
Tactic:
assumption
State after:
no goals