Theorem: SciLean.Scalar.log.arg_x.revDeriv_rule_at (SciLean/Core/Functions/Exp.lean)

State before:
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ revDeriv R (fun u => log (x u)) u =
    let xdx := revDeriv R x u;
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
Tactic:
unfold revDeriv
State after:
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ ((fun u => log (x u)) u, semiAdjoint R (cderiv R (fun u => log (x u)) u)) =
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))

State before:
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ ((fun u => log (x u)) u, semiAdjoint R (cderiv R (fun u => log (x u)) u)) =
    let xdx := (x u, semiAdjoint R (cderiv R x u));
    (log xdx.1, fun dy => xdx.2 ((abs (x u))⁻¹ * dy))
Tactic:
fun_trans (disch:=aesop) only [fwdDeriv, smul_push, ftrans_simp]
State after:
no goals

State before:
case funProp.discharger
R✝ : Type ?u.26877
C : Type ?u.26876
inst✝⁶ : Scalar R✝ C
inst✝⁵ : RealScalar R✝
W✝ : Type ?u.26886
inst✝⁴ : Vec C W✝
U✝ : Type ?u.26909
inst✝³ : SemiInnerProductSpace C U✝
R : Type u_1
inst✝² : RealScalar R
W : Type ?u.26931
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiInnerProductSpace R U
u : U
x : U → R
hx : HasAdjDiffAt R x u
hu : x u ≠ 0
⊢ x u ≠ 0
Tactic:
aesop
State after:
no goals