simpa only [e3] using continuous_self_div_sq_add_sq hy
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
hy : y ≠ 0
f : ℝ → ℝ := fun x => (x ^ 2 + y ^ 2).log / 2
e1 : ∀ {x : ℝ}, HasDerivAt (fun x => x ^ 2 + y ^ 2) (2 * x) x
e2 : ∀ {x : ℝ}, HasDerivAt f (x / (x ^ 2 + y ^ 2)) x
e3 : deriv f = fun x => x / (x ^ 2 + y ^ 2)
⊢ Continuous (deriv f)
no goals