r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = toIocMod two_pi_pos (-π) θ
r : ℝ
hr : 0 < r
θ : ℝ
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = toIocMod two_pi_pos (-π) θ
have hi : toIocMod Real.two_pi_pos (-π) θ ∈ Set.Ioc (-π) π := by
  convert toIocMod_mem_Ioc _ _ θ
  ring
case h.e'_2.h.e'_1.h.e'_6
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
⊢ cos ↑θ + sin ↑θ * I = cos ↑(toIocMod two_pi_pos (-π) θ) + sin ↑(toIocMod two_pi_pos (-π) θ) * I
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = toIocMod two_pi_pos (-π) θ
convert arg_mul_cos_add_sin_mul_I hr hi using 3
no goals
case h.e'_2.h.e'_1.h.e'_6
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
⊢ cos ↑θ + sin ↑θ * I = cos ↑(toIocMod two_pi_pos (-π) θ) + sin ↑(toIocMod two_pi_pos (-π) θ) * I
simp [toIocMod, cos_sub_int_mul_two_pi, sin_sub_int_mul_two_pi]
case h.e'_5.h.e'_4
r : ℝ
hr : 0 < r
θ : ℝ
⊢ π = -π + 2 * π
r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
convert toIocMod_mem_Ioc _ _ θ
no goals
case h.e'_5.h.e'_4
r : ℝ
hr : 0 < r
θ : ℝ
⊢ π = -π + 2 * π
ring