case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log (↑abs z)) - ↑π * I) = 𝓝 ((ofReal' ∘ fun x => Real.log (↑abs x)) z + ↑(-π) * I)

case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log (↑abs z)) - ↑π * I))
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_abs.continuousWithinAt.log _)).tendsto.add
    (((continuous_ofReal.tendsto _).comp <|
          tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using 1
no goals
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log (↑abs z)) - ↑π * I) = 𝓝 ((ofReal' ∘ fun x => Real.log (↑abs x)) z + ↑(-π) * I)
simp [sub_eq_add_neg]
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
lift z to ℝ using him
no goals
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
simpa using hre.ne