[GOAL]
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
⊢ arg ↑(↑expMapCircle x) = x
[PROOFSTEP]
rw [expMapCircle_apply, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]
[GOAL]
x y : ℝ
⊢ ↑expMapCircle x = ↑expMapCircle y ↔ ∃ m, x = y + ↑m * (2 * π)
[PROOFSTEP]
rw [Subtype.ext_iff, expMapCircle_apply, expMapCircle_apply, exp_eq_exp_iff_exists_int]
[GOAL]
x y : ℝ
⊢ (∃ n, ↑x * I = ↑y * I + ↑n * (2 * ↑π * I)) ↔ ∃ m, x = y + ↑m * (2 * π)
[PROOFSTEP]
refine' exists_congr fun n => _
[GOAL]
x y : ℝ
n : ℤ
⊢ ↑x * I = ↑y * I + ↑n * (2 * ↑π * I) ↔ x = y + ↑n * (2 * π)
[PROOFSTEP]
rw [← mul_assoc, ← add_mul, mul_left_inj' I_ne_zero]
[GOAL]
x y : ℝ
n : ℤ
⊢ ↑x = ↑y + ↑n * (2 * ↑π) ↔ x = y + ↑n * (2 * π)
[PROOFSTEP]
norm_cast
[GOAL]
z : ℝ
⊢ z + 2 * π = z + ↑1 * (2 * π)
[PROOFSTEP]
rw [Int.cast_one, one_mul]
[GOAL]
θ : Angle
⊢ ↑(expMapCircle θ) = ↑(cos θ) + ↑(sin θ) * I
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ ↑(expMapCircle ↑x✝) = ↑(cos ↑x✝) + ↑(sin ↑x✝) * I
[PROOFSTEP]
simp [Complex.exp_mul_I]
[GOAL]
⊢ expMapCircle 0 = 1
[PROOFSTEP]
rw [← Real.Angle.coe_zero, Real.Angle.expMapCircle_coe, _root_.expMapCircle_zero]
[GOAL]
θ : Angle
⊢ expMapCircle (-θ) = (expMapCircle θ)⁻¹
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ expMapCircle (-↑x✝) = (expMapCircle ↑x✝)⁻¹
[PROOFSTEP]
simp_rw [← Real.Angle.coe_neg, Real.Angle.expMapCircle_coe, _root_.expMapCircle_neg]
[GOAL]
θ₁ θ₂ : Angle
⊢ expMapCircle (θ₁ + θ₂) = expMapCircle θ₁ * expMapCircle θ₂
[PROOFSTEP]
induction θ₁ using Real.Angle.induction_on
[GOAL]
case h
θ₂ : Angle
x✝ : ℝ
⊢ expMapCircle (↑x✝ + θ₂) = expMapCircle ↑x✝ * expMapCircle θ₂
[PROOFSTEP]
induction θ₂ using Real.Angle.induction_on
[GOAL]
case h.h
x✝¹ x✝ : ℝ
⊢ expMapCircle (↑x✝¹ + ↑x✝) = expMapCircle ↑x✝¹ * expMapCircle ↑x✝
[PROOFSTEP]
exact _root_.expMapCircle_add _ _
[GOAL]
θ : Angle
⊢ ↑(arg ↑(expMapCircle θ)) = θ
[PROOFSTEP]
induction θ using Real.Angle.induction_on
[GOAL]
case h
x✝ : ℝ
⊢ ↑(arg ↑(expMapCircle ↑x✝)) = ↑x✝
[PROOFSTEP]
rw [Real.Angle.expMapCircle_coe, expMapCircle_apply, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ← Real.Angle.cos_coe, ←
  Real.Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]
