Theorem: SciLean.Scalar.sin.arg_x.revDeriv_rule (SciLean/Core/Functions/Trigonometric.lean)

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

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