x : ℂ
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
x : ℂ
⊢ arg (↑(starRingEnd ℂ) x) = if arg x = π then π else -arg x
simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, abs_conj, neg_div, neg_neg,
  Real.arcsin_neg, apply_ite Neg.neg, neg_add, neg_sub, neg_neg, ← sub_eq_add_neg, sub_neg_eq_add,
  add_comm π]
case inl.inl
x : ℂ
hr : x.re < 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inl.inr.inl
x : ℂ
hr : x.re < 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inl.inr.inr
x : ℂ
hr : x.re < 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inr.inl.inl
x : ℂ
hr : x.re = 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inr.inl.inr.inl
x : ℂ
hr : x.re = 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inr.inl.inr.inr
x : ℂ
hr : x.re = 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π

case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
x : ℂ
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
rcases lt_trichotomy x.re 0 with (hr | hr | hr) <;>
  rcases lt_trichotomy x.im 0 with (hi | hi | hi)
no goals
case inl.inl
x : ℂ
hr : x.re < 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr, hr.not_le, hi.le, hi.ne, not_le.2 hi, add_comm]
no goals
case inl.inr.inl
x : ℂ
hr : x.re < 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr, hr.not_le, hi]
no goals
case inl.inr.inr
x : ℂ
hr : x.re < 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr, hr.not_le, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]
no goals
case inr.inl.inl
x : ℂ
hr : x.re = 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr]
no goals
case inr.inl.inr.inl
x : ℂ
hr : x.re = 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr]
no goals
case inr.inl.inr.inr
x : ℂ
hr : x.re = 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr]
no goals
case inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr, hr.le, hi.ne]
no goals
case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr, hr.le, hr.le.not_lt]
no goals
case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
simp [hr, hr.le, hr.le.not_lt]