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

State before:
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
⊢ 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:
unfold revDeriv
State after:
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')))

State before:
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')))
Tactic:
fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
State after:
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))))

State before:
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))))
Tactic:
simp
State after:
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 y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * y)) = fun dy =>
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))

State before:
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 y => semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * y)) = fun dy =>
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))
Tactic:
funext dy
State after:
case h
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
dy : R
⊢ semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * dy) =
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))

State before:
case h
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
dy : R
⊢ semiAdjoint R (fun x_1 => cderiv R (fun w => x w) u x_1) ((sqrt (x u))⁻¹ * 2⁻¹ * dy) =
    semiAdjoint R (cderiv R x u) (dy / (2 * sqrt (x u)))
Tactic:
congr
State after:
case h.e_y
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
dy : R
⊢ (sqrt (x u))⁻¹ * 2⁻¹ * dy = dy / (2 * sqrt (x u))

State before:
case h.e_y
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
dy : R
⊢ (sqrt (x u))⁻¹ * 2⁻¹ * dy = dy / (2 * sqrt (x u))
Tactic:
field_simp [mul_comm]
State after:
no goals

State before:
case funProp.discharger
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
⊢ 0 < x u
Tactic:
aesop
State after:
no goals