z : ℂ
hπ : 0 < π
⊢ arg z ∈ Set.Ioc (-π) π
z : ℂ
⊢ arg z ∈ Set.Ioc (-π) π
have hπ : 0 < π := Real.pi_pos
case inl
hπ : 0 < π
⊢ arg 0 ∈ Set.Ioc (-π) π

case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ arg z ∈ Set.Ioc (-π) π
z : ℂ
hπ : 0 < π
⊢ arg z ∈ Set.Ioc (-π) π
rcases eq_or_ne z 0 with (rfl | hz)
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ arg z ∈ Set.Ioc (-π) π
case inl
hπ : 0 < π
⊢ arg 0 ∈ Set.Ioc (-π) π

case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ arg z ∈ Set.Ioc (-π) π
simp [hπ, hπ.le]
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + N • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ arg z ∈ Set.Ioc (-π) π
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ arg z ∈ Set.Ioc (-π) π
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg z ∈ Set.Ioc (-π) π
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + N • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ arg z ∈ Set.Ioc (-π) π
rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg z ∈ Set.Ioc (-π) π
rw [← abs_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
simp only [← ofReal_one, ← ofReal_bit0, ← ofReal_mul, ← ofReal_add, ofReal_int_cast]
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
this : arg (↑(↑abs z) * (cos ↑(arg z + ↑N * (2 * π)) + sin ↑(arg z + ↑N * (2 * π)) * I)) = arg z + ↑N * (2 * π)
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
have := arg_mul_cos_add_sin_mul_I (abs.pos hz) hN
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
this : arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) = arg z + ↑N * (2 * π)
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
this : arg (↑(↑abs z) * (cos ↑(arg z + ↑N * (2 * π)) + sin ↑(arg z + ↑N * (2 * π)) * I)) = arg z + ↑N * (2 * π)
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
push_cast at this
no goals
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
this : arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) = arg z + ↑N * (2 * π)
⊢ arg (↑(↑abs z) * (cos (↑(arg z) + ↑N * (2 * ↑π)) + sin (↑(arg z) + ↑N * (2 * ↑π)) * I)) ∈ Set.Ioc (-π) π
rwa [this]