fun_trans
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => ((fun w => cos (x w)) x_1, cderiv C (fun w => cos (x w)) x_1 dx)) = fun w dw =>
    let xdx := (x w, cderiv C x w dw);
    let s := sin xdx.1;
    let c := cos xdx.1;
    (c, xdx.2 * -s)
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.8066
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (cos (x x_1), -((fwdDeriv C (fun w => x w) x_1 dx).2 * sin (fwdDeriv C (fun w => x w) x_1 dx).1))) =
    fun w dw => (cos (x w), -(cderiv C x w dw * sin (x w)))