rfl
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type u_2
inst✝¹ : Vec C W
U : Type ?u.725
inst✝ : SemiInnerProductSpace C U
x : W → C
hx : CDifferentiable C x
⊢ (fun x_1 dx => (sin (x x_1), (fwdDeriv C (fun w => x w) x_1 dx).2 * cos (fwdDeriv C (fun w => x w) x_1 dx).1)) =
    fun w dw => (sin (x w), cderiv C x w dw * cos (x w))
no goals