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

State before:
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
⊢ (revDeriv R fun u => sqrt (x u)) = fun u =>
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Tactic:
funext u
State after:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ revDeriv R (fun u => sqrt (x u)) u =
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))

State before:
case h
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.50858
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
x : U → R
hx : HasAdjDiff R x
hu : ∀ (u : U), 0 < x u
u : U
⊢ revDeriv R (fun u => sqrt (x u)) u =
    let xdx := revDeriv R x u;
    let x' := sqrt xdx.1;
    (x', fun dy => xdx.2 (dy / (2 * x')))
Tactic:
fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
State after:
no goals

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