Derivative_of_Sine_Function
Provedderivative-of-sine-functionderivatives-of-trigonometric-functionsproofwikisine-function
The derivative of sin(x) is cos(x).
Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv import Mathlib.Tactic variable (x : ℝ)
Formal statement
theorem Derivative_of_Sine_Function : HasDerivAt Real.sin (Real.cos x) x := by sorry
Source