case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z | 0 ≤ z.im} z
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_abs.continuousWithinAt.log _)).tendsto.add
    ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
          continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using 1
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