x : ℂ
hx : x ≠ 0
⊢ Real.cos
      (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.re / ↑abs x
x : ℂ
hx : x ≠ 0
⊢ Real.cos (arg x) = x.re / ↑abs x
rw [arg]
case inl
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (arcsin (x.im / ↑abs x)) = x.re / ↑abs x

case inr.inl
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (arcsin ((-x).im / ↑abs x) + π) = x.re / ↑abs x

case inr.inr
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (arcsin ((-x).im / ↑abs x) - π) = x.re / ↑abs x
x : ℂ
hx : x ≠ 0
⊢ Real.cos
      (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.re / ↑abs x
split_ifs with h₁ h₂
case inl
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ sqrt (1 - (x.im / ↑abs x) ^ 2) = x.re / ↑abs x
case inl
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (arcsin (x.im / ↑abs x)) = x.re / ↑abs x
rw [Real.cos_arcsin]
no goals
case inl
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ sqrt (1 - (x.im / ↑abs x) ^ 2) = x.re / ↑abs x
simp [Real.sqrt_sq, (abs.pos hx).le, *, one_sub_div]
case inr.inl
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -sqrt (1 - ((-x).im / ↑abs x) ^ 2) = x.re / ↑abs x
case inr.inl
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (arcsin ((-x).im / ↑abs x) + π) = x.re / ↑abs x
rw [Real.cos_add_pi, Real.cos_arcsin]
no goals
case inr.inl
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -sqrt (1 - ((-x).im / ↑abs x) ^ 2) = x.re / ↑abs x
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁),
  *, one_sub_div, neg_div]
case inr.inr
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -sqrt (1 - ((-x).im / ↑abs x) ^ 2) = x.re / ↑abs x
case inr.inr
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (arcsin ((-x).im / ↑abs x) - π) = x.re / ↑abs x
rw [Real.cos_sub_pi, Real.cos_arcsin]
no goals
case inr.inr
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -sqrt (1 - ((-x).im / ↑abs x) ^ 2) = x.re / ↑abs x
simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁),
  *, one_sub_div, neg_div]