r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ (if 0 ≤ (↑r * (cos ↑θ + sin ↑θ * I)).re then arcsin ((↑r * (cos ↑θ + sin ↑θ * I)).im / r)
    else
      if 0 ≤ (↑r * (cos ↑θ + sin ↑θ * I)).im then arcsin ((-(↑r * (cos ↑θ + sin ↑θ * I))).im / r) + π
      else arcsin ((-(↑r * (cos ↑θ + sin ↑θ * I))).im / r) - π) =
    θ
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = θ
simp only [arg, map_mul, abs_cos_add_sin_mul_I, abs_of_nonneg hr.le, mul_one]
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ (if 0 ≤ (↑r * (cos ↑θ + sin ↑θ * I)).re then arcsin ((↑r * (cos ↑θ + sin ↑θ * I)).im / r)
    else
      if 0 ≤ (↑r * (cos ↑θ + sin ↑θ * I)).im then arcsin ((-(↑r * (cos ↑θ + sin ↑θ * I))).im / r) + π
      else arcsin ((-(↑r * (cos ↑θ + sin ↑θ * I))).im / r) - π) =
    θ
simp only [ofReal_mul_re, ofReal_mul_im, neg_im, ← ofReal_cos, ← ofReal_sin, ←
  mk_eq_add_mul_I, neg_div, mul_div_cancel_left _ hr.ne', mul_nonneg_iff_right_nonneg_of_pos hr]
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ

case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : ¬θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ arcsin (Real.sin θ) = θ

case pos.hc
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ Real.cos θ
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
rw [if_pos]
no goals
case pos
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ arcsin (Real.sin θ) = θ

case pos.hc
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ Real.cos θ
exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁]
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : ¬θ ∈ Set.Icc (-(π / 2)) (π / 2)
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ < -(π / 2)
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ

case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
cases' h₁ with h₁ h₁
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : θ < -(π / 2)
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
replace hθ := hθ.1
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
have hcos : Real.cos θ < 0 := by
  rw [← neg_pos, ← Real.cos_add_pi]
  refine' Real.cos_pos_of_mem_Ioo ⟨_, _⟩ <;> linarith
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
no goals
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel] <;> [linarith;
  linarith; exact hsin.not_le; exact hcos.not_le]
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ Real.cos θ < 0
rw [← neg_pos, ← Real.cos_add_pi]
no goals
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)
refine' Real.cos_pos_of_mem_Ioo ⟨_, _⟩ <;> linarith
no goals
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ θ < 0
linarith
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
h₁ : π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
replace hθ := hθ.2
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
no goals
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ (if 0 ≤ Real.cos θ then arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then arcsin (-Real.sin θ) + π else arcsin (-Real.sin θ) - π) =
    θ
rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
  linarith; exact hsin; exact hcos.not_le]
no goals
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ θ < π + π / 2
linarith
no goals
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ 0 ≤ θ
linarith