case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(arg (↑r * (↑(Angle.cos ↑θ) + ↑(Angle.sin ↑θ) * I))) = ↑θ
r : ℝ
hr : 0 < r
θ : Angle
⊢ ↑(arg (↑r * (↑(Angle.cos θ) + ↑(Angle.sin θ) * I))) = θ
induction' θ using Real.Angle.induction_on with θ
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ∃ k, arg (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)) - θ = 2 * π * ↑k
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(arg (↑r * (↑(Angle.cos ↑θ) + ↑(Angle.sin ↑θ) * I))) = ↑θ
rw [Real.Angle.cos_coe, Real.Angle.sin_coe, Real.Angle.angle_eq_iff_two_pi_dvd_sub]
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ arg (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)) - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ∃ k, arg (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)) - θ = 2 * π * ↑k
use ⌊(π - θ) / (2 * π)⌋
no goals
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ arg (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)) - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
exact_mod_cast arg_mul_cos_add_sin_mul_I_sub hr θ