Theorem: SciLean.Scalar.tanh.arg_x.fwdDeriv_rule (SciLean/Core/Functions/Trigonometric.lean)

State before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fwdDeriv C fun w => tanh (x w)) = fun w dw =>
    let xdx := fwdDeriv C x w dw;
    let t := tanh xdx.1;
    let dt := 1 - t ^ 2;
    (t, xdx.2 * dt)
Tactic:
unfold fwdDeriv
State after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => tanh (x w)) x_1, cderiv C (fun w => tanh (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let t := tanh xdx.1;
    let dt := 1 - t ^ 2;
    (t, xdx.2 * dt)

State before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => tanh (x w)) x_1, cderiv C (fun w => tanh (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let t := tanh xdx.1;
    let dt := 1 - t ^ 2;
    (t, xdx.2 * dt)
Tactic:
fun_trans
State after:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx =>
      (tanh (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * (1 - tanh (fwdDeriv C (fun w => x w) x_1 dx).1 ^ 2))) =
    fun w dw => (tanh (x w), cderiv C x w dw * (1 - tanh (x w) ^ 2))

State before:
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.17106
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx =>
      (tanh (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * (1 - tanh (fwdDeriv C (fun w => x w) x_1 dx).1 ^ 2))) =
    fun w dw => (tanh (x w), cderiv C x w dw * (1 - tanh (x w) ^ 2))
Tactic:
rfl
State after:
no goals