x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0
refine' ⟨fun hc h₀ => _, fun h => (hasDerivAt_tan h).continuousAt⟩
no goals
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _
  (hc.norm.tendsto.mono_left inf_le_left)