Derivative_of_Arctangent_Function_v2
Provedarctangent-functionderivative-of-arctangent-functionderivatives-of-inverse-trigonometric-functionsproofwiki
The derivative of the tangent function at x is 1/cos^2(x), which for arctan gives d/dx(arctan x) = 1/(1+x^2).
Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.Analysis.Calculus.Deriv.Basic
Formal statement
theorem Derivative_of_Arctangent_Function_v2 (x : ℝ) (hx : Real.cos x ≠ 0) : HasDerivAt Real.tan (1 / (Real.cos x) ^ 2) x := by sorry
Source