x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
x : ℝ
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
no goals
x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
simpa [cos_sq_arctan] using
  tanLocalHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)
no goals
x : ℝ
A : cos (arctan x) ≠ 0
⊢ ↑1 / cos (↑(LocalHomeomorph.symm tanLocalHomeomorph) x) ^ 2 ≠ 0
simpa