[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (↑1 / cos x ^ 2) x
[PROOFSTEP]
exact_mod_cast (Complex.hasStrictDerivAt_tan (by exact_mod_cast h)).real_of_complex
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt tan (↑1 / cos x ^ 2) x
[PROOFSTEP]
exact_mod_cast (Complex.hasDerivAt_tan (by exact_mod_cast h)).real_of_complex
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x : ℝ
hx : cos x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
have hx : Complex.cos x = 0 := by exact_mod_cast hx
[GOAL]
x : ℝ
hx : cos x = 0
⊢ Complex.cos ↑x = 0
[PROOFSTEP]
exact_mod_cast hx
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => |tan x|) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
simp only [← Complex.abs_ofReal, Complex.ofReal_tan]
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑Complex.abs (Complex.tan ↑x)) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
refine' (Complex.tendsto_abs_tan_of_cos_eq_zero hx).comp _
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓝[{x}ᶜ] x) (𝓝[{↑x}ᶜ] ↑x)
[PROOFSTEP]
refine' Tendsto.inf Complex.continuous_ofReal.continuousAt _
[GOAL]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓟 {x}ᶜ) (𝓟 {↑x}ᶜ)
[PROOFSTEP]
exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1
[GOAL]
x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0
[PROOFSTEP]
refine' ⟨fun hc h₀ => _, fun h => (hasDerivAt_tan h).continuousAt⟩
[GOAL]
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
[PROOFSTEP]
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _ (hc.norm.tendsto.mono_left inf_le_left)
[GOAL]
x : ℝ
h : cos x = 0
⊢ deriv tan x = ↑1 / cos x ^ 2
[PROOFSTEP]
have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
[GOAL]
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = ↑1 / cos x ^ 2
[PROOFSTEP]
simp [deriv_zero_of_not_differentiableAt this, h, sq]
[GOAL]
n : ℕ∞
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x : ℝ
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
[PROOFSTEP]
have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
[GOAL]
x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (↑1 / (↑1 + x ^ 2)) x
[PROOFSTEP]
simpa [cos_sq_arctan] using tanLocalHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)
[GOAL]
x : ℝ
A : cos (arctan x) ≠ 0
⊢ ↑1 / cos (↑(LocalHomeomorph.symm tanLocalHomeomorph) x) ^ 2 ≠ 0
[PROOFSTEP]
simpa
[GOAL]
n : ℕ∞
x : ℝ
this : cos (arctan x) ≠ 0
⊢ ↑1 / cos (↑(LocalHomeomorph.symm tanLocalHomeomorph) x) ^ 2 ≠ 0
[PROOFSTEP]
simpa
