[GOAL]
x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (↑1 / cos x ^ 2) x
[PROOFSTEP]
convert (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1
[GOAL]
case h.e'_7
x : ℂ
h : cos x ≠ 0
⊢ ↑1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
[PROOFSTEP]
rw_mod_cast [← sin_sq_add_cos_sq x]
[GOAL]
case h.e'_7
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
[PROOFSTEP]
ring
[GOAL]
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ↑abs (tan x)) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
simp only [tan_eq_sin_div_cos, ← norm_eq_abs, norm_div]
[GOAL]
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x
[GOAL]
x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False
[PROOFSTEP]
simpa [*, sq] using sin_sq_add_cos_sq x
[GOAL]
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) := hx ▸ (hasDerivAt_cos x).tendsto_punctured_nhds (neg_ne_zero.2 A)
[GOAL]
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[{x}ᶜ] x) (𝓝[{0}ᶜ] 0)
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
[PROOFSTEP]
exact
  continuous_sin.continuousWithinAt.norm.mul_atTop (norm_pos_iff.2 A)
    (tendsto_norm_nhdsWithin_zero.comp B).inv_tendsto_zero
[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]
