no goals
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log (↑abs z)) + ↑π * I))
simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using
  (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto