no goals
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt tan (↑1 / cos x ^ 2) x
exact_mod_cast (Complex.hasDerivAt_tan (by exact_mod_cast h)).real_of_complex
no goals
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
exact_mod_cast h