x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => abs (tan x)) (𝓝[{x}ᶜ] x) atTop
x : ℝ
hx : cos x = 0
⊢ Tendsto (fun x => abs (tan x)) (𝓝[{x}ᶜ] x) atTop
have hx : Complex.cos x = 0 := by exact_mod_cast hx
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑Complex.abs (Complex.tan ↑x)) (𝓝[{x}ᶜ] x) atTop
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => abs (tan x)) (𝓝[{x}ᶜ] x) atTop
simp only [← Complex.abs_ofReal, Complex.ofReal_tan]
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓝[{x}ᶜ] x) (𝓝[{↑x}ᶜ] ↑x)
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑Complex.abs (Complex.tan ↑x)) (𝓝[{x}ᶜ] x) atTop
refine' (Complex.tendsto_abs_tan_of_cos_eq_zero hx).comp _
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓟 ({x}ᶜ)) (𝓟 ({↑x}ᶜ))
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓝[{x}ᶜ] x) (𝓝[{↑x}ᶜ] ↑x)
refine' Tendsto.inf Complex.continuous_ofReal.continuousAt _
no goals
x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto (fun x => ↑x) (𝓟 ({x}ᶜ)) (𝓟 ({↑x}ᶜ))
exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1
no goals
x : ℝ
hx : cos x = 0
⊢ Complex.cos ↑x = 0
exact_mod_cast hx