x : ℂ
⊢ Real.sin
      (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.im / ↑abs x
x : ℂ
⊢ Real.sin (arg x) = x.im / ↑abs x
unfold arg
no goals
x : ℂ
⊢ Real.sin
      (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.im / ↑abs x
split_ifs <;>
simp [sub_eq_add_neg, arg,
Real.sin_arcsin (abs_le.1 (abs_im_div_abs_le_one x)).1 (abs_le.1 (abs_im_div_abs_le_one x)).2,
Real.sin_add, neg_div, Real.arcsin_neg, Real.sin_neg]