x : ℂ
⊢ ↑(Real.log (↑abs x)) + ↑(if arg x = π then π else -arg x) * I =
    if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
x : ℂ
⊢ log (↑(starRingEnd ℂ) x) = if arg x = π then log x else ↑(starRingEnd ℂ) (log x)
simp_rw [log, abs_conj, arg_conj, map_add, map_mul, conj_ofReal]
case inl
x : ℂ
hx : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑π * I = ↑(Real.log (↑abs x)) + ↑(arg x) * I

case inr
x : ℂ
hx : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(-arg x) * I = ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
x : ℂ
⊢ ↑(Real.log (↑abs x)) + ↑(if arg x = π then π else -arg x) * I =
    if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
split_ifs with hx
no goals
case inr
x : ℂ
hx : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(-arg x) * I = ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]
no goals
case inl
x : ℂ
hx : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑π * I = ↑(Real.log (↑abs x)) + ↑(arg x) * I
rw [hx]