x y : ℝ
⊢ ContinuousAt log x → x ≠ 0
x y : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0
refine' ⟨_, continuousAt_log⟩
y : ℝ
h : ContinuousAt log 0
⊢ False
x y : ℝ
⊢ ContinuousAt log x → x ≠ 0
rintro h rfl
no goals
y : ℝ
h : ContinuousAt log 0
⊢ False
exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsWithin_zero _
  (h.tendsto.mono_left inf_le_left)