-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_inv_eq_ite (x : ℂ) : log x⁻¹ = if x.arg = π then -conj (log x) else -log x

Proof state:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - 2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Tactic:
rw [two_mul]

Result:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) -
      (↑(Real.log ‖x‖) + ↑(Real.log ‖x‖)) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Proof state:
case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]

Result:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0

Proof state:
case pos
x : ℂ
hx : x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
simp [hx]

Result:
no goals

Proof state:
x : ℂ
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
by_cases hx : x = 0

Result:
case pos
x : ℂ
hx : x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Proof state:
case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

Tactic:
rwa [inv_pos, Complex.normSq_pos]

Result:
no goals

Proof state:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - ↑2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Tactic:
norm_num

Result:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - 2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Proof state:
case pos
x : ℂ
hx : ¬x = 0
h✝ : x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑x.arg * I - (↑(Real.log ‖x‖) + ↑(Real.log ‖x‖)) = -↑(Real.log ‖x‖) + ↑x.arg * I

Tactic:
rw [add_sub_right_comm, sub_add_cancel_left]

Result:
no goals

Proof state:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) -
      (↑(Real.log ‖x‖) + ↑(Real.log ‖x‖)) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Tactic:
split_ifs

Result:
case pos
x : ℂ
hx : ¬x = 0
h✝ : x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑x.arg * I - (↑(Real.log ‖x‖) + ↑(Real.log ‖x‖)) = -↑(Real.log ‖x‖) + ↑x.arg * I

case neg
x : ℂ
hx : ¬x = 0
h✝ : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + -(↑x.arg * I) - (↑(Real.log ‖x‖) + ↑(Real.log ‖x‖)) = -↑(Real.log ‖x‖) + -(↑x.arg * I)

Proof state:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_norm_sq, Real.log_pow,
  Nat.cast_two, ofReal_mul, neg_add, mul_neg, neg_neg]

Result:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else ↑(Real.log ‖x‖) + -(↑x.arg * I)) - ↑2 * ↑(Real.log ‖x‖) =
    if x.arg = π then -↑(Real.log ‖x‖) + ↑x.arg * I else -↑(Real.log ‖x‖) + -(↑x.arg * I)

Proof state:
case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0

Tactic:
rwa [map_ne_zero]

Result:
no goals

Proof state:
case neg
x : ℂ
hx : ¬x = 0
h✝ : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + -(↑x.arg * I) - (↑(Real.log ‖x‖) + ↑(Real.log ‖x‖)) = -↑(Real.log ‖x‖) + -(↑x.arg * I)

Tactic:
rw [add_sub_right_comm, sub_add_cancel_left]

Result:
no goals