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

case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
x : ℂ
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
by_cases hx : x = 0
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) - ↑(Real.log (↑normSq x)) =
    if arg x = π 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
case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
no goals
case pos
x : ℂ
hx : x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
simp [hx]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      ↑2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) - ↑(Real.log (↑normSq x)) =
    if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_abs, Real.log_pow,
  Nat.cast_two, ofReal_mul, ofReal_bit0, ofReal_one, neg_add, mul_neg, two_mul, neg_neg]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      ↑2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
norm_num
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
rw [two_mul]
case neg.inl
x : ℂ
hx : ¬x = 0
h✝ : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(arg x) * I - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + ↑(arg x) * I

case neg.inr
x : ℂ
hx : ¬x = 0
h✝ : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + -(↑(arg x) * I) - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
split_ifs
no goals
case neg.inl
x : ℂ
hx : ¬x = 0
h✝ : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(arg x) * I - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + ↑(arg x) * I
rw [add_sub_right_comm, sub_add_cancel']
no goals
case neg.inr
x : ℂ
hx : ¬x = 0
h✝ : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + -(↑(arg x) * I) - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
rw [add_sub_right_comm, sub_add_cancel']
no goals
case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (↑normSq x)⁻¹
rwa [inv_pos, Complex.normSq_pos]
no goals
case neg.hx
x : ℂ
hx : ¬x = 0
⊢ ↑(starRingEnd ℂ) x ≠ 0
rwa [map_ne_zero]