Theorem: SciLean.Scalar.exp.arg_x.revDeriv_rule (SciLean/Core/Functions/Exp.lean)

State before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.5049
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (revDeriv C fun u => exp (x u)) = fun u =>
    let xdx := revDeriv C x u;
    (exp xdx.1, fun dy => xdx.2 ((starRingEnd C) (exp xdx.1) * dy))
Tactic:
unfold revDeriv
State after:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.5049
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => exp (x u)) x_1, semiAdjoint C (cderiv C (fun u => exp (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (exp xdx.1, fun dy => xdx.2 ((starRingEnd C) (exp xdx.1) * dy))

State before:
R : Type u_3
C : Type u_1
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.5049
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x : U → C
hx : HasAdjDiff C x
⊢ (fun x_1 => ((fun u => exp (x u)) x_1, semiAdjoint C (cderiv C (fun u => exp (x u)) x_1))) = fun u =>
    let xdx := (x u, semiAdjoint C (cderiv C x u));
    (exp xdx.1, fun dy => xdx.2 ((starRingEnd C) (exp xdx.1) * dy))
Tactic:
fun_trans only [fwdDeriv, smul_push, ftrans_simp]
State after:
no goals