x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ↑abs (tan x)) (𝓝[{x}ᶜ] x) atTop
simp only [tan_eq_sin_div_cos, ← norm_eq_abs, norm_div]
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x
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
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto (fun x => ‖sin x‖ / ‖cos x‖) (𝓝[{x}ᶜ] x) atTop
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) :=
  hx ▸ (hasDerivAt_cos x).tendsto_punctured_nhds (neg_ne_zero.2 A)
no goals
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
exact continuous_sin.continuousWithinAt.norm.mul_atTop (norm_pos_iff.2 A)
  (tendsto_norm_nhdsWithin_zero.comp B).inv_tendsto_zero
no goals
x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False
simpa [*, sq] using sin_sq_add_cos_sq x