[GOAL]
x : ℂ
⊢ Real.sin (arg x) = x.im / ↑abs x
[PROOFSTEP]
unfold arg
[GOAL]
x : ℂ
⊢ Real.sin
      (if 0 ≤ x.re then arcsin (x.im / ↑abs x)
      else if 0 ≤ x.im then arcsin ((-x).im / ↑abs x) + π else arcsin ((-x).im / ↑abs x) - π) =
    x.im / ↑abs x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℂ
h✝ : 0 ≤ x.re
⊢ Real.sin (arcsin (x.im / ↑abs x)) = x.im / ↑abs x
[PROOFSTEP]
simp [sub_eq_add_neg, arg,
  Real.sin_arcsin (abs_le.1 (abs_im_div_abs_le_one x)).1 (abs_le.1 (abs_im_div_abs_le_one x)).2, Real.sin_add, neg_div,
  Real.arcsin_neg, Real.sin_neg]
[GOAL]
case pos
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : 0 ≤ x.im
⊢ Real.sin (arcsin ((-x).im / ↑abs x) + π) = x.im / ↑abs x
[PROOFSTEP]
simp [sub_eq_add_neg, arg,
  Real.sin_arcsin (abs_le.1 (abs_im_div_abs_le_one x)).1 (abs_le.1 (abs_im_div_abs_le_one x)).2, Real.sin_add, neg_div,
  Real.arcsin_neg, Real.sin_neg]
[GOAL]
case neg
x : ℂ
h✝¹ : ¬0 ≤ x.re
h✝ : ¬0 ≤ x.im
⊢ Real.sin (arcsin ((-x).im / ↑abs x) - π) = x.im / ↑abs x
[PROOFSTEP]
simp [sub_eq_add_neg, arg,
  Real.sin_arcsin (abs_le.1 (abs_im_div_abs_le_one x)).1 (abs_le.1 (abs_im_div_abs_le_one x)).2, Real.sin_add, neg_div,
  Real.arcsin_neg, Real.sin_neg]
[GOAL]
x : ℂ
hx : x ≠ 0
⊢ Real.cos (arg x) = x.re / ↑abs x
[PROOFSTEP]
rw [arg]
[GOAL]
x : ℂ
hx : x ≠ 0
⊢ Real.cos
      (if 0 ≤ x.re then arcsin (x.im / ↑abs x)
      else if 0 ≤ x.im then arcsin ((-x).im / ↑abs x) + π else arcsin ((-x).im / ↑abs x) - π) =
    x.re / ↑abs x
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ Real.cos (arcsin (x.im / ↑abs x)) = x.re / ↑abs x
[PROOFSTEP]
rw [Real.cos_arcsin]
[GOAL]
case pos
x : ℂ
hx : x ≠ 0
h₁ : 0 ≤ x.re
⊢ sqrt (1 - (x.im / ↑abs x) ^ 2) = x.re / ↑abs x
[PROOFSTEP]
field_simp [Real.sqrt_sq, (abs.pos hx).le, *]
[GOAL]
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ Real.cos (arcsin ((-x).im / ↑abs x) + π) = x.re / ↑abs x
[PROOFSTEP]
rw [Real.cos_add_pi, Real.cos_arcsin]
[GOAL]
case pos
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : 0 ≤ x.im
⊢ -sqrt (1 - ((-x).im / ↑abs x) ^ 2) = x.re / ↑abs x
[PROOFSTEP]
field_simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
[GOAL]
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ Real.cos (arcsin ((-x).im / ↑abs x) - π) = x.re / ↑abs x
[PROOFSTEP]
rw [Real.cos_sub_pi, Real.cos_arcsin]
[GOAL]
case neg
x : ℂ
hx : x ≠ 0
h₁ : ¬0 ≤ x.re
h₂ : ¬0 ≤ x.im
⊢ -sqrt (1 - ((-x).im / ↑abs x) ^ 2) = x.re / ↑abs x
[PROOFSTEP]
field_simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
[GOAL]
x : ℂ
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
⊢ ↑(↑abs 0) * exp (↑(arg 0) * I) = 0
[PROOFSTEP]
simp
[GOAL]
case inr
x : ℂ
hx : x ≠ 0
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
[PROOFSTEP]
have : abs x ≠ 0 := abs.ne_zero hx
[GOAL]
case inr
x : ℂ
hx : x ≠ 0
this : ↑abs x ≠ 0
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
[PROOFSTEP]
ext
[GOAL]
case inr.a
x : ℂ
hx : x ≠ 0
this : ↑abs x ≠ 0
⊢ (↑(↑abs x) * exp (↑(arg x) * I)).re = x.re
[PROOFSTEP]
field_simp [sin_arg, cos_arg hx, this, mul_comm (abs x)]
[GOAL]
case inr.a
x : ℂ
hx : x ≠ 0
this : ↑abs x ≠ 0
⊢ (↑(↑abs x) * exp (↑(arg x) * I)).im = x.im
[PROOFSTEP]
field_simp [sin_arg, cos_arg hx, this, mul_comm (abs x)]
[GOAL]
x : ℂ
⊢ ↑(↑abs x) * (cos ↑(arg x) + sin ↑(arg x) * I) = x
[PROOFSTEP]
rw [← exp_mul_I, abs_mul_exp_arg_mul_I]
[GOAL]
z : ℂ
⊢ ↑abs z = 1 ↔ ∃ θ, exp (↑θ * I) = z
[PROOFSTEP]
refine' ⟨fun hz => ⟨arg z, _⟩, _⟩
[GOAL]
case refine'_1
z : ℂ
hz : ↑abs z = 1
⊢ exp (↑(arg z) * I) = z
[PROOFSTEP]
calc
  exp (arg z * I) = abs z * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
  _ = z := abs_mul_exp_arg_mul_I z
[GOAL]
z : ℂ
hz : ↑abs z = 1
⊢ exp (↑(arg z) * I) = ↑(↑abs z) * exp (↑(arg z) * I)
[PROOFSTEP]
rw [hz, ofReal_one, one_mul]
[GOAL]
case refine'_2
z : ℂ
⊢ (∃ θ, exp (↑θ * I) = z) → ↑abs z = 1
[PROOFSTEP]
rintro ⟨θ, rfl⟩
[GOAL]
case refine'_2.intro
θ : ℝ
⊢ ↑abs (exp (↑θ * I)) = 1
[PROOFSTEP]
exact Complex.abs_exp_ofReal_mul_I θ
[GOAL]
⊢ (Set.range fun x => exp (↑x * I)) = Metric.sphere 0 1
[PROOFSTEP]
ext x
[GOAL]
case h
x : ℂ
⊢ (x ∈ Set.range fun x => exp (↑x * I)) ↔ x ∈ Metric.sphere 0 1
[PROOFSTEP]
simp only [mem_sphere_zero_iff_norm, norm_eq_abs, abs_eq_one_iff, Set.mem_range]
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = θ
[PROOFSTEP]
simp only [arg, map_mul, abs_cos_add_sin_mul_I, abs_of_nonneg hr.le, mul_one]
[GOAL]
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) - π) =
    θ
[PROOFSTEP]
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]
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
rw [if_pos]
[GOAL]
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 θ
[PROOFSTEP]
exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁]
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁ 
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
cases' h₁ with h₁ h₁
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
replace hθ := hθ.1
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
have hcos : Real.cos θ < 0 := by
  rw [← neg_pos, ← Real.cos_add_pi]
  refine' Real.cos_pos_of_mem_Ioo ⟨_, _⟩ <;> linarith
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ Real.cos θ < 0
[PROOFSTEP]
rw [← neg_pos, ← Real.cos_add_pi]
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)
[PROOFSTEP]
refine' Real.cos_pos_of_mem_Ioo ⟨_, _⟩
[GOAL]
case refine'_1
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ -(π / 2) < θ + π
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ θ + π < π / 2
[PROOFSTEP]
linarith
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ θ < 0
[PROOFSTEP]
linarith
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
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]
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel]
[GOAL]
case neg.inl.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ -(π / 2) ≤ θ + π
[PROOFSTEP]
linarith
[GOAL]
case neg.inl.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ
[PROOFSTEP]
exact hsin.not_le
[GOAL]
case neg.inl.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ
[PROOFSTEP]
exact hcos.not_le
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
replace hθ := hθ.2
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ θ < π + π / 2
[PROOFSTEP]
linarith
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ 0 ≤ θ
[PROOFSTEP]
linarith
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith; linarith; exact hsin;
  exact hcos.not_le]
[GOAL]
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 θ) - π) =
    θ
[PROOFSTEP]
rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel]
[GOAL]
case neg.inr.hx₁
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ -(π / 2) ≤ θ - π
[PROOFSTEP]
linarith
[GOAL]
case neg.inr.hx₂
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ θ - π ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
case neg.inr.hc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ 0 ≤ Real.sin θ
[PROOFSTEP]
exact hsin
[GOAL]
case neg.inr.hnc
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ
[PROOFSTEP]
exact hcos.not_le
[GOAL]
θ : ℝ
hθ : θ ∈ Set.Ioc (-π) π
⊢ arg (cos ↑θ + sin ↑θ * I) = θ
[PROOFSTEP]
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]
[GOAL]
⊢ arg 0 = 0
[PROOFSTEP]
simp [arg, le_refl]
[GOAL]
x y : ℂ
h₁ : ↑abs x = ↑abs y
h₂ : arg x = arg y
⊢ x = y
[PROOFSTEP]
rw [← abs_mul_exp_arg_mul_I x, ← abs_mul_exp_arg_mul_I y, h₁, h₂]
[GOAL]
z : ℂ
⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
have hπ : 0 < π := Real.pi_pos
[GOAL]
z : ℂ
hπ : 0 < π
⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz)
[GOAL]
case inl
hπ : 0 < π
⊢ arg 0 ∈ Set.Ioc (-π) π
case inr z : ℂ hπ : 0 < π hz : z ≠ 0 ⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
simp [hπ, hπ.le]
[GOAL]
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩
[GOAL]
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + N • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN 
[GOAL]
case inr.intro.intro
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : arg z + ↑N * (2 * π) ∈ Set.Ioc (-π) π
⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]
[GOAL]
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 (-π) π
[PROOFSTEP]
simp only [← ofReal_one, ← ofReal_bit0, ← ofReal_mul, ← ofReal_add, ofReal_int_cast]
[GOAL]
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 (-π) π
[PROOFSTEP]
have := arg_mul_cos_add_sin_mul_I (abs.pos hz) hN
[GOAL]
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 (-π) π
[PROOFSTEP]
push_cast at this 
[GOAL]
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 (-π) π
[PROOFSTEP]
rwa [this]
[GOAL]
z : ℂ
⊢ 0 ≤ arg z ↔ 0 ≤ z.im
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | h₀)
[GOAL]
case inl
⊢ 0 ≤ arg 0 ↔ 0 ≤ 0.im
[PROOFSTEP]
simp
[GOAL]
case inr
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ arg z ↔ 0 ≤ z.im
[PROOFSTEP]
calc
  0 ≤ arg z ↔ 0 ≤ Real.sin (arg z) :=
    ⟨fun h => Real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩,
      by
      contrapose!
      intro h
      exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)⟩
  _ ↔ _ := by rw [sin_arg, le_div_iff (abs.pos h₀), zero_mul]
[GOAL]
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin (arg z) → 0 ≤ arg z
[PROOFSTEP]
contrapose!
[GOAL]
z : ℂ
h₀ : z ≠ 0
⊢ arg z < 0 → Real.sin (arg z) < 0
[PROOFSTEP]
intro h
[GOAL]
z : ℂ
h₀ : z ≠ 0
h : arg z < 0
⊢ Real.sin (arg z) < 0
[PROOFSTEP]
exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)
[GOAL]
z : ℂ
h₀ : z ≠ 0
⊢ 0 ≤ Real.sin (arg z) ↔ 0 ≤ z.im
[PROOFSTEP]
rw [sin_arg, le_div_iff (abs.pos h₀), zero_mul]
[GOAL]
x : ℂ
r : ℝ
hr : 0 < r
⊢ arg (↑r * x) = arg x
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
r : ℝ
hr : 0 < r
⊢ arg (↑r * 0) = arg 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ arg (↑r * x) = arg x
[PROOFSTEP]
conv_lhs =>
  rw [← abs_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
    arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc]
[GOAL]
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| arg (↑r * x)
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
    arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc]
[GOAL]
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| arg (↑r * x)
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
    arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc]
[GOAL]
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
| arg (↑r * x)
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
  arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc]
[GOAL]
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ arg x = arg y ↔ ↑(↑abs y) / ↑(↑abs x) * x = y
[PROOFSTEP]
simp only [ext_abs_arg_iff, map_mul, map_div₀, abs_ofReal, abs_abs, div_mul_cancel _ (abs.ne_zero hx), eq_self_iff_true,
  true_and_iff]
[GOAL]
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ arg x = arg y ↔ arg (↑(↑abs y) / ↑(↑abs x) * x) = arg y
[PROOFSTEP]
rw [← ofReal_div, arg_real_mul]
[GOAL]
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ↑abs y / ↑abs x
[PROOFSTEP]
exact div_pos (abs.pos hy) (abs.pos hx)
[GOAL]
⊢ arg 1 = 0
[PROOFSTEP]
simp [arg, zero_le_one]
[GOAL]
⊢ arg (-1) = π
[PROOFSTEP]
simp [arg, le_refl, not_le.2 (zero_lt_one' ℝ)]
[GOAL]
⊢ arg I = π / 2
[PROOFSTEP]
simp [arg, le_refl]
[GOAL]
⊢ arg (-I) = -(π / 2)
[PROOFSTEP]
simp [arg, le_refl]
[GOAL]
x : ℂ
⊢ Real.tan (arg x) = x.im / x.re
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
x : ℂ
h : x = 0
⊢ Real.tan (arg x) = x.im / x.re
[PROOFSTEP]
simp only [h, zero_div, Complex.zero_im, Complex.arg_zero, Real.tan_zero, Complex.zero_re]
[GOAL]
case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan (arg x) = x.im / x.re
[PROOFSTEP]
rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h, div_div_div_cancel_right _ (abs.ne_zero h)]
[GOAL]
x : ℝ
hx : 0 ≤ x
⊢ arg ↑x = 0
[PROOFSTEP]
simp [arg, hx]
[GOAL]
z : ℂ
⊢ arg z = 0 ↔ 0 ≤ z.re ∧ z.im = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
z : ℂ
h : arg z = 0
⊢ 0 ≤ z.re ∧ z.im = 0
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I z, h]
[GOAL]
case refine'_1
z : ℂ
h : arg z = 0
⊢ 0 ≤ (↑(↑abs z) * (cos ↑0 + sin ↑0 * I)).re ∧ (↑(↑abs z) * (cos ↑0 + sin ↑0 * I)).im = 0
[PROOFSTEP]
simp [abs.nonneg]
[GOAL]
case refine'_2
z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 → arg z = 0
[PROOFSTEP]
cases' z with x y
[GOAL]
case refine'_2.mk
x y : ℝ
⊢ 0 ≤ { re := x, im := y }.re ∧ { re := x, im := y }.im = 0 → arg { re := x, im := y } = 0
[PROOFSTEP]
rintro ⟨h, rfl : y = 0⟩
[GOAL]
case refine'_2.mk.intro
x : ℝ
h : 0 ≤ { re := x, im := 0 }.re
⊢ arg { re := x, im := 0 } = 0
[PROOFSTEP]
exact arg_ofReal_of_nonneg h
[GOAL]
z : ℂ
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
[PROOFSTEP]
by_cases h₀ : z = 0
[GOAL]
case pos
z : ℂ
h₀ : z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
case neg z : ℂ h₀ : ¬z = 0 ⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
[PROOFSTEP]
simp [h₀, lt_irrefl, Real.pi_ne_zero.symm]
[GOAL]
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π ↔ z.re < 0 ∧ z.im = 0
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π → z.re < 0 ∧ z.im = 0
[PROOFSTEP]
intro h
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π
⊢ z.re < 0 ∧ z.im = 0
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I z, h]
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π
⊢ (↑(↑abs z) * (cos ↑π + sin ↑π * I)).re < 0 ∧ (↑(↑abs z) * (cos ↑π + sin ↑π * I)).im = 0
[PROOFSTEP]
simp [h₀]
[GOAL]
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → arg z = π
[PROOFSTEP]
cases' z with x y
[GOAL]
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re < 0 ∧ { re := x, im := y }.im = 0 → arg { re := x, im := y } = π
[PROOFSTEP]
rintro ⟨h : x < 0, rfl : y = 0⟩
[GOAL]
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ arg { re := x, im := 0 } = π
[PROOFSTEP]
rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
[GOAL]
case neg.mpr.mk.intro
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ arg { re := x, im := 0 } = arg (↑(-x) * -1)
[PROOFSTEP]
simp [← ofReal_def]
[GOAL]
z : ℂ
⊢ arg z < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
[PROOFSTEP]
rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]
[GOAL]
z : ℂ
⊢ arg z = π / 2 ↔ z.re = 0 ∧ 0 < z.im
[PROOFSTEP]
by_cases h₀ : z = 0
[GOAL]
case pos
z : ℂ
h₀ : z = 0
⊢ arg z = π / 2 ↔ z.re = 0 ∧ 0 < z.im
[PROOFSTEP]
simp [h₀, lt_irrefl, Real.pi_div_two_pos.ne]
[GOAL]
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π / 2 ↔ z.re = 0 ∧ 0 < z.im
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = π / 2 → z.re = 0 ∧ 0 < z.im
[PROOFSTEP]
intro h
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π / 2
⊢ z.re = 0 ∧ 0 < z.im
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I z, h]
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = π / 2
⊢ (↑(↑abs z) * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑(↑abs z) * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im
[PROOFSTEP]
simp [h₀]
[GOAL]
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → arg z = π / 2
[PROOFSTEP]
cases' z with x y
[GOAL]
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ 0 < { re := x, im := y }.im → arg { re := x, im := y } = π / 2
[PROOFSTEP]
rintro ⟨rfl : x = 0, hy : 0 < y⟩
[GOAL]
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ arg { re := 0, im := y } = π / 2
[PROOFSTEP]
rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
[GOAL]
z : ℂ
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
[PROOFSTEP]
by_cases h₀ : z = 0
[GOAL]
case pos
z : ℂ
h₀ : z = 0
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
[PROOFSTEP]
simp [h₀, lt_irrefl, Real.pi_ne_zero]
[GOAL]
case neg
z : ℂ
h₀ : ¬z = 0
⊢ arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ arg z = -(π / 2) → z.re = 0 ∧ z.im < 0
[PROOFSTEP]
intro h
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = -(π / 2)
⊢ z.re = 0 ∧ z.im < 0
[PROOFSTEP]
rw [← abs_mul_cos_add_sin_mul_I z, h]
[GOAL]
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : arg z = -(π / 2)
⊢ (↑(↑abs z) * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧
    (↑(↑abs z) * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0
[PROOFSTEP]
simp [h₀]
[GOAL]
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → arg z = -(π / 2)
[PROOFSTEP]
cases' z with x y
[GOAL]
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → arg { re := x, im := y } = -(π / 2)
[PROOFSTEP]
rintro ⟨rfl : x = 0, hy : y < 0⟩
[GOAL]
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ arg { re := 0, im := y } = -(π / 2)
[PROOFSTEP]
rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]
[GOAL]
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ arg (↑0 + ↑y * I) = arg (↑(-y) * -I)
[PROOFSTEP]
simp
[GOAL]
x : ℂ
hx_re : x.re < 0
hx_im : 0 ≤ x.im
⊢ arg x = arcsin ((-x).im / ↑abs x) + π
[PROOFSTEP]
simp only [arg, hx_re.not_le, hx_im, if_true, if_false]
[GOAL]
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ arg x = arcsin ((-x).im / ↑abs x) - π
[PROOFSTEP]
simp only [arg, hx_re.not_le, hx_im.not_le, if_false]
[GOAL]
z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
⊢ arg z = arccos (z.re / ↑abs z)
[PROOFSTEP]
rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]
[GOAL]
z : ℂ
hz : z.im < 0
⊢ arg z = -arccos (z.re / ↑abs z)
[PROOFSTEP]
have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne
[GOAL]
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ arg z = -arccos (z.re / ↑abs z)
[PROOFSTEP]
rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg]
[GOAL]
case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -arg z
case hx₂ z : ℂ hz : z.im < 0 h₀ : z ≠ 0 ⊢ -arg z ≤ π
[PROOFSTEP]
exacts [neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le]
[GOAL]
x : ℂ
⊢ arg (↑(starRingEnd ℂ) x) = if arg x = π then π else -arg x
[PROOFSTEP]
simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, abs_conj, neg_div, neg_neg, Real.arcsin_neg]
[GOAL]
x : ℂ
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
[GOAL]
case inl
x : ℂ
hr : x.re < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
[GOAL]
case inr.inl
x : ℂ
hr : x.re = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
[GOAL]
case inr.inr
x : ℂ
hr : 0 < x.re
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
[GOAL]
case inl.inl
x : ℂ
hr : x.re < 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr, hr.not_le, hi.le, hi.ne, not_le.2 hi, add_comm]
[GOAL]
case inl.inr.inl
x : ℂ
hr : x.re < 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr, hr.not_le, hi]
[GOAL]
case inl.inr.inr
x : ℂ
hr : x.re < 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr, hr.not_le, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]
[GOAL]
case inr.inl.inl
x : ℂ
hr : x.re = 0
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr]
[GOAL]
case inr.inl.inr.inl
x : ℂ
hr : x.re = 0
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr]
[GOAL]
case inr.inl.inr.inr
x : ℂ
hr : x.re = 0
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr]
[GOAL]
case inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im < 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr, hr.le, hi.ne]
[GOAL]
case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr, hr.le, hr.le.not_lt]
[GOAL]
case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -arcsin (x.im / ↑abs x)
    else if 0 ≤ -x.im then arcsin (x.im / ↑abs x) + π else arcsin (x.im / ↑abs x) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then arcsin (x.im / ↑abs x)
        else if 0 ≤ x.im then -arcsin (x.im / ↑abs x) + π else -arcsin (x.im / ↑abs x) - π
[PROOFSTEP]
simp [hr, hr.le, hr.le.not_lt]
[GOAL]
x : ℂ
⊢ arg x⁻¹ = if arg x = π then π else -arg x
[PROOFSTEP]
rw [← arg_conj, inv_def, mul_comm]
[GOAL]
x : ℂ
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x : ℂ
hx : x = 0
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ arg (↑(↑normSq x)⁻¹ * ↑(starRingEnd ℂ) x) = arg (↑(starRingEnd ℂ) x)
[PROOFSTEP]
exact arg_real_mul (conj x) (by simp [hx])
[GOAL]
x : ℂ
hx : ¬x = 0
⊢ 0 < (↑normSq x)⁻¹
[PROOFSTEP]
simp [hx]
[GOAL]
z : ℂ
⊢ arg z ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
[PROOFSTEP]
cases' le_or_lt 0 (re z) with hre hre
[GOAL]
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ arg z ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
[PROOFSTEP]
simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or_iff]
[GOAL]
case inr
z : ℂ
hre : z.re < 0
⊢ arg z ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
[PROOFSTEP]
simp only [hre.not_le, false_or_iff]
[GOAL]
case inr
z : ℂ
hre : z.re < 0
⊢ arg z ≤ π / 2 ↔ z.im < 0
[PROOFSTEP]
cases' le_or_lt 0 (im z) with him him
[GOAL]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ arg z ≤ π / 2 ↔ z.im < 0
[PROOFSTEP]
simp only [him.not_lt]
[GOAL]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ arg z ≤ π / 2 ↔ False
[PROOFSTEP]
rw [iff_false_iff, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
  Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ← _root_.abs_of_nonneg him, abs_im_lt_abs]
[GOAL]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0
case inr.inl z : ℂ hre : z.re < 0 him : 0 ≤ z.im ⊢ 0 < ↑abs z
[PROOFSTEP]
exacts [hre.ne, abs.pos <| ne_of_apply_ne re hre.ne]
[GOAL]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arg z ≤ π / 2 ↔ z.im < 0
[PROOFSTEP]
simp only [him]
[GOAL]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arg z ≤ π / 2 ↔ True
[PROOFSTEP]
rw [iff_true_iff, arg_of_re_neg_of_im_neg hre him]
[GOAL]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ arcsin ((-z).im / ↑abs z) - π ≤ π / 2
[PROOFSTEP]
exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)
[GOAL]
z : ℂ
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
[PROOFSTEP]
cases' le_or_lt 0 (re z) with hre hre
[GOAL]
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
[PROOFSTEP]
simp only [hre, arg_of_re_nonneg hre, Real.neg_pi_div_two_le_arcsin, true_or_iff]
[GOAL]
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.re ∨ 0 ≤ z.im
[PROOFSTEP]
simp only [hre.not_le, false_or_iff]
[GOAL]
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
[PROOFSTEP]
cases' le_or_lt 0 (im z) with him him
[GOAL]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
[PROOFSTEP]
simp only [him]
[GOAL]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arg z ↔ True
[PROOFSTEP]
rw [iff_true_iff, arg_of_re_neg_of_im_nonneg hre him]
[GOAL]
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ arcsin ((-z).im / ↑abs z) + π
[PROOFSTEP]
exact (Real.neg_pi_div_two_le_arcsin _).trans (le_add_of_nonneg_right Real.pi_pos.le)
[GOAL]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ arg z ↔ 0 ≤ z.im
[PROOFSTEP]
simp only [him.not_le]
[GOAL]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ arg z ↔ False
[PROOFSTEP]
rw [iff_false_iff, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ← sub_eq_add_neg, sub_half,
  Real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him, abs_im_lt_abs]
[GOAL]
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0
case inr.inr z : ℂ hre : z.re < 0 him : z.im < 0 ⊢ 0 < ↑abs z
[PROOFSTEP]
exacts [hre.ne, abs.pos <| ne_of_apply_ne re hre.ne]
[GOAL]
z : ℂ
⊢ |arg z| ≤ π / 2 ↔ 0 ≤ z.re
[PROOFSTEP]
rw [abs_le, arg_le_pi_div_two_iff, neg_pi_div_two_le_arg_iff, ← or_and_left, ← not_le, and_not_self_iff, or_false_iff]
[GOAL]
x : ℂ
⊢ ↑(arg (↑(starRingEnd ℂ) x)) = -↑(arg x)
[PROOFSTEP]
by_cases h : arg x = π
[GOAL]
case pos
x : ℂ
h : arg x = π
⊢ ↑(arg (↑(starRingEnd ℂ) x)) = -↑(arg x)
[PROOFSTEP]
simp [arg_conj, h]
[GOAL]
case neg
x : ℂ
h : ¬arg x = π
⊢ ↑(arg (↑(starRingEnd ℂ) x)) = -↑(arg x)
[PROOFSTEP]
simp [arg_conj, h]
[GOAL]
x : ℂ
⊢ ↑(arg x⁻¹) = -↑(arg x)
[PROOFSTEP]
by_cases h : arg x = π
[GOAL]
case pos
x : ℂ
h : arg x = π
⊢ ↑(arg x⁻¹) = -↑(arg x)
[PROOFSTEP]
simp [arg_inv, h]
[GOAL]
case neg
x : ℂ
h : ¬arg x = π
⊢ ↑(arg x⁻¹) = -↑(arg x)
[PROOFSTEP]
simp [arg_inv, h]
[GOAL]
x : ℂ
hi : 0 < x.im
⊢ arg (-x) = arg x - π
[PROOFSTEP]
rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]
[GOAL]
x : ℂ
hi : 0 < x.im
⊢ -arccos ((-x).re / ↑abs (-x)) = arccos (x.re / ↑abs x) - π
[PROOFSTEP]
simp [neg_div, Real.arccos_neg]
[GOAL]
x : ℂ
hi : x.im < 0
⊢ arg (-x) = arg x + π
[PROOFSTEP]
rw [arg_of_im_neg hi, arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)]
[GOAL]
x : ℂ
hi : x.im < 0
⊢ arccos ((-x).re / ↑abs (-x)) = -arccos (x.re / ↑abs x) + π
[PROOFSTEP]
simp [neg_div, Real.arccos_neg, add_comm, ← sub_eq_add_neg]
[GOAL]
x : ℂ
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
[PROOFSTEP]
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
[GOAL]
case inl
x : ℂ
hi : x.im < 0
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
[PROOFSTEP]
simp [hi, hi.ne, hi.not_lt, arg_neg_eq_arg_add_pi_of_im_neg, sub_eq_add_neg, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
[GOAL]
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
[PROOFSTEP]
rw [(ext rfl hi : x = x.re)]
[GOAL]
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
[PROOFSTEP]
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
[GOAL]
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
[PROOFSTEP]
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
[GOAL]
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
[PROOFSTEP]
simp [hr]
[GOAL]
case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
[PROOFSTEP]
simp [hr, hi, Real.pi_ne_zero]
[GOAL]
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ arg (-↑x.re) = arg ↑x.re - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
[PROOFSTEP]
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
[GOAL]
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
[PROOFSTEP]
simp [hr.not_lt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]
[GOAL]
case inr.inr
x : ℂ
hi : 0 < x.im
⊢ arg (-x) = arg x - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
[PROOFSTEP]
simp [hi, arg_neg_eq_arg_sub_pi_of_im_pos]
[GOAL]
x : ℂ
⊢ arg (-x) = arg x + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
[PROOFSTEP]
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
[GOAL]
case inl
x : ℂ
hi : x.im < 0
⊢ arg (-x) = arg x + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
[PROOFSTEP]
simp [hi, arg_neg_eq_arg_add_pi_of_im_neg]
[GOAL]
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-x) = arg x + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
[PROOFSTEP]
rw [(ext rfl hi : x = x.re)]
[GOAL]
case inr.inl
x : ℂ
hi : x.im = 0
⊢ arg (-↑x.re) = arg ↑x.re + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
[PROOFSTEP]
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
[GOAL]
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ arg (-↑x.re) = arg ↑x.re + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
[PROOFSTEP]
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]
[GOAL]
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
[PROOFSTEP]
simp [hr.not_lt, ← two_mul, Real.pi_ne_zero]
[GOAL]
case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ arg (-↑x.re) = arg ↑x.re + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
[PROOFSTEP]
simp [hr, hi, Real.pi_ne_zero.symm]
[GOAL]
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ arg (-↑x.re) = arg ↑x.re + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
[PROOFSTEP]
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
[GOAL]
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
[PROOFSTEP]
simp [hr]
[GOAL]
case inr.inr
x : ℂ
hi : 0 < x.im
⊢ arg (-x) = arg x + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
[PROOFSTEP]
simp [hi, hi.ne.symm, hi.not_lt, arg_neg_eq_arg_sub_pi_of_im_pos, sub_eq_add_neg, ← add_eq_zero_iff_neg_eq,
  Real.pi_ne_zero]
[GOAL]
x : ℂ
hx : x ≠ 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
[PROOFSTEP]
rcases lt_trichotomy x.im 0 with (hi | hi | hi)
[GOAL]
case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
[PROOFSTEP]
rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]
[GOAL]
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
[PROOFSTEP]
rw [(ext rfl hi : x = x.re)]
[GOAL]
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
[PROOFSTEP]
rcases lt_trichotomy x.re 0 with (hr | hr | hr)
[GOAL]
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
[PROOFSTEP]
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le, ← Real.Angle.coe_add, ←
  two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]
[GOAL]
case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
[PROOFSTEP]
exact False.elim (hx (ext hr hi))
[GOAL]
case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(arg (-↑x.re)) = ↑(arg ↑x.re) + ↑π
[PROOFSTEP]
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr), Real.Angle.coe_zero, zero_add]
[GOAL]
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(arg (-x)) = ↑(arg x) + ↑π
[PROOFSTEP]
rw [arg_neg_eq_arg_sub_pi_of_im_pos hi, Real.Angle.coe_sub, Real.Angle.sub_coe_pi_eq_add_coe_pi]
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = toIocMod two_pi_pos (-π) θ
[PROOFSTEP]
have hi : toIocMod Real.two_pi_pos (-π) θ ∈ Set.Ioc (-π) π :=
  by
  convert toIocMod_mem_Ioc _ _ θ
  ring
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
[PROOFSTEP]
convert toIocMod_mem_Ioc _ _ θ
[GOAL]
case h.e'_5.h.e'_4
r : ℝ
hr : 0 < r
θ : ℝ
⊢ π = -π + 2 * π
[PROOFSTEP]
ring
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod two_pi_pos (-π) θ ∈ Set.Ioc (-π) π
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) = toIocMod two_pi_pos (-π) θ
[PROOFSTEP]
convert arg_mul_cos_add_sin_mul_I hr hi using 3
[GOAL]
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
[PROOFSTEP]
simp [toIocMod, cos_sub_int_mul_two_pi, sin_sub_int_mul_two_pi]
[GOAL]
θ : ℝ
⊢ arg (cos ↑θ + sin ↑θ * I) = toIocMod two_pi_pos (-π) θ
[PROOFSTEP]
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
⊢ arg (↑r * (cos ↑θ + sin ↑θ * I)) - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
[PROOFSTEP]
rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor, zsmul_eq_mul]
[GOAL]
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
[PROOFSTEP]
ring_nf
[GOAL]
θ : ℝ
⊢ arg (cos ↑θ + sin ↑θ * I) - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
[PROOFSTEP]
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]
[GOAL]
r : ℝ
hr : 0 < r
θ : Angle
⊢ ↑(arg (↑r * (↑(Angle.cos θ) + ↑(Angle.sin θ) * I))) = θ
[PROOFSTEP]
induction' θ using Real.Angle.induction_on with θ
[GOAL]
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(arg (↑r * (↑(Angle.cos ↑θ) + ↑(Angle.sin ↑θ) * I))) = ↑θ
[PROOFSTEP]
rw [Real.Angle.cos_coe, Real.Angle.sin_coe, Real.Angle.angle_eq_iff_two_pi_dvd_sub]
[GOAL]
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ∃ k, arg (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)) - θ = 2 * π * ↑k
[PROOFSTEP]
use⌊(π - θ) / (2 * π)⌋
[GOAL]
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ arg (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)) - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
[PROOFSTEP]
exact_mod_cast arg_mul_cos_add_sin_mul_I_sub hr θ
[GOAL]
θ : Angle
⊢ ↑(arg (↑(Angle.cos θ) + ↑(Angle.sin θ) * I)) = θ
[PROOFSTEP]
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]
[GOAL]
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(arg (x * y)) = ↑(arg x) + ↑(arg y)
[PROOFSTEP]
convert arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (abs.pos hx) (abs.pos hy)) (arg x + arg y : Real.Angle) using 3
[GOAL]
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(↑abs x * ↑abs y) * (↑(Angle.cos (↑(arg x) + ↑(arg y))) + ↑(Angle.sin (↑(arg x) + ↑(arg y))) * I)
[PROOFSTEP]
simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin, cos_add_sin_I,
  ofReal_add, add_mul, exp_add, ofReal_mul]
[GOAL]
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(↑abs x) * ↑(↑abs y) * (exp (↑(arg x) * I) * exp (↑(arg y) * I))
[PROOFSTEP]
rw [mul_assoc, mul_comm (exp _), ← mul_assoc (abs y : ℂ), abs_mul_exp_arg_mul_I, mul_comm y, ← mul_assoc,
  abs_mul_exp_arg_mul_I]
[GOAL]
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(arg (x / y)) = ↑(arg x) - ↑(arg y)
[PROOFSTEP]
rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]
[GOAL]
z : ℂ
⊢ Angle.toReal ↑(arg z) = arg z
[PROOFSTEP]
rw [Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
[GOAL]
z : ℂ
⊢ arg z ∈ Set.Ioc (-π) π
[PROOFSTEP]
exact arg_mem_Ioc _
[GOAL]
z : ℂ
θ : Angle
⊢ ↑(arg z) = θ ↔ arg z = Angle.toReal θ
[PROOFSTEP]
rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]
[GOAL]
x y : ℂ
⊢ ↑(arg x) = ↑(arg y) ↔ arg x = arg y
[PROOFSTEP]
simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]
[GOAL]
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) + π
[PROOFSTEP]
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im
[GOAL]
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
h_forall_nhds : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) + π
case h_forall_nhds x z : ℂ hx_re : x.re < 0 hx_im : 0 < x.im ⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
[PROOFSTEP]
exact h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le
[GOAL]
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
[PROOFSTEP]
refine' IsOpen.eventually_mem _ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)
[GOAL]
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen fun y => y.re < 0 ∧ 0 < y.im
[PROOFSTEP]
exact IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)
[GOAL]
x z : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) - π
[PROOFSTEP]
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ y.im < 0
[GOAL]
x z : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
h_forall_nhds : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) - π
case h_forall_nhds x z : ℂ hx_re : x.re < 0 hx_im : x.im < 0 ⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
[PROOFSTEP]
exact h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_neg hy.1 hy.2
[GOAL]
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
[PROOFSTEP]
refine' IsOpen.eventually_mem _ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)
[GOAL]
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ IsOpen fun y => y.re < 0 ∧ y.im < 0
[PROOFSTEP]
exact IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)
[GOAL]
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt arg x
[PROOFSTEP]
have h₀ : abs x ≠ 0 := by
  rw [abs.ne_zero_iff]
  rintro rfl
  simp at h 
[GOAL]
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ↑abs x ≠ 0
[PROOFSTEP]
rw [abs.ne_zero_iff]
[GOAL]
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
z : ℂ
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
⊢ ContinuousAt arg x
[PROOFSTEP]
rw [← lt_or_lt_iff_ne] at h 
[GOAL]
x z : ℂ
h✝ : 0 < x.re ∨ x.im ≠ 0
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ↑abs x ≠ 0
⊢ ContinuousAt arg x
[PROOFSTEP]
rcases h with (hx_re | hx_im | hx_im)
[GOAL]
case inl
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x
case inr.inl
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_im : x.im < 0
⊢ ContinuousAt arg x
case inr.inr x z : ℂ h : 0 < x.re ∨ x.im ≠ 0 h₀ : ↑abs x ≠ 0 hx_im : 0 < x.im ⊢ ContinuousAt arg x
[PROOFSTEP]
exacts
  [(Real.continuousAt_arcsin.comp (continuous_im.continuousAt.div continuous_abs.continuousAt h₀)).congr
    (arg_eq_nhds_of_re_pos hx_re).symm,
  (Real.continuous_arccos.continuousAt.comp (continuous_re.continuousAt.div continuous_abs.continuousAt h₀)).neg.congr
    (arg_eq_nhds_of_im_neg hx_im).symm,
  (Real.continuous_arccos.continuousAt.comp (continuous_re.continuousAt.div continuous_abs.continuousAt h₀)).congr
    (arg_eq_nhds_of_im_pos hx_im).symm]
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
[PROOFSTEP]
suffices H : Tendsto (fun x : ℂ => Real.arcsin ((-x).im / abs x) - π) (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
[PROOFSTEP]
refine' H.congr' _
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ (fun x => arcsin ((-x).im / ↑abs x) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg
[PROOFSTEP]
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 :=
  continuous_re.tendsto z
    (gt_mem_nhds hre)
      -- Porting note: need to specify the `nhdsWithin` set
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ (fun x => arcsin ((-x).im / ↑abs x) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin (s := {z : ℂ | z.im < 0}), mem_nhdsWithin_of_mem_nhds this] with _ him hre
[GOAL]
case h
x z✝ z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ arcsin ((-a✝).im / ↑abs a✝) - π = arg a✝
[PROOFSTEP]
rw [arg, if_neg hre.not_le, if_neg him.not_le]
[GOAL]
case H
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
[PROOFSTEP]
convert
  (Real.continuousAt_arcsin.comp_continuousWithinAt
        ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
          continuous_abs.continuousWithinAt (s := {z : ℂ | z.im < 0}) (_ : abs z ≠ 0))
          -- Porting note: specify constant precisely to assist in goal below).sub_const
    π using
  1
[GOAL]
case h.e'_5
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((arcsin ∘ (im ∘ Neg.neg / ↑abs)) z - π)
[PROOFSTEP]
simp [him]
[GOAL]
case H
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
[PROOFSTEP]
lift z to ℝ using him
[GOAL]
case H.intro
x z✝ : ℂ
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
[PROOFSTEP]
simpa using hre.ne
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z
[PROOFSTEP]
have : arg =ᶠ[𝓝[{z : ℂ | 0 ≤ z.im}] z] fun x => Real.arcsin ((-x).im / abs x) + π :=
  by
  have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
  filter_upwards [self_mem_nhdsWithin (s := {z : ℂ | 0 ≤ z.im}), mem_nhdsWithin_of_mem_nhds this] with _ him hre
  rw [arg, if_neg hre.not_le, if_pos him]
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
[PROOFSTEP]
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin (s := {z : ℂ | 0 ≤ z.im}), mem_nhdsWithin_of_mem_nhds this] with _ him hre
[GOAL]
case h
x z✝ z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ arg a✝ = arcsin ((-a✝).im / ↑abs a✝) + π
[PROOFSTEP]
rw [arg, if_neg hre.not_le, if_pos him]
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z
[PROOFSTEP]
refine' ContinuousWithinAt.congr_of_eventuallyEq _ this _
[GOAL]
case refine'_1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ContinuousWithinAt (fun x => arcsin ((-x).im / ↑abs x) + π) {z | 0 ≤ z.im} z
[PROOFSTEP]
refine'
  (Real.continuousAt_arcsin.comp_continuousWithinAt
        ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
          continuous_abs.continuousWithinAt _)).add
    tendsto_const_nhds
[GOAL]
case refine'_1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ↑abs z ≠ 0
[PROOFSTEP]
lift z to ℝ using him
[GOAL]
case refine'_1.intro
x z✝ : ℂ
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ↑abs ↑z ≠ 0
[PROOFSTEP]
simpa using hre.ne
[GOAL]
case refine'_2
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ arg z = arcsin ((-z).im / ↑abs z) + π
[PROOFSTEP]
rw [arg, if_neg hre.not_le, if_pos him.ge]
[GOAL]
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | 0 ≤ z.im}] z) (𝓝 π)
[PROOFSTEP]
simpa only [arg_eq_pi_iff.2 ⟨hre, him⟩] using (continuousWithinAt_arg_of_re_neg_of_im_zero hre him).tendsto
[GOAL]
x z : ℂ
h : x ≠ 0
⊢ ContinuousAt (Angle.coe ∘ arg) x
[PROOFSTEP]
by_cases hs : 0 < x.re ∨ x.im ≠ 0
[GOAL]
case pos
x z : ℂ
h : x ≠ 0
hs : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (Angle.coe ∘ arg) x
[PROOFSTEP]
exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (Angle.coe ∘ arg) x
[PROOFSTEP]
rw [← Function.comp.right_id (((↑) : ℝ → Real.Angle) ∘ arg),
  (Function.funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ← Function.comp.assoc]
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (((Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
[PROOFSTEP]
refine' ContinuousAt.comp _ continuous_neg.continuousAt
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt ((Angle.coe ∘ arg) ∘ Neg.neg) (-x)
[PROOFSTEP]
suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
  rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this 
[GOAL]
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
this : ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
⊢ ContinuousAt ((Angle.coe ∘ arg) ∘ Neg.neg) (-x)
[PROOFSTEP]
rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this 
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
[PROOFSTEP]
have ha : Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π = fun z => (arg z : Real.Angle) + π :=
  by
  rw [Function.update_eq_iff]
  exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
[GOAL]
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
[PROOFSTEP]
rw [Function.update_eq_iff]
[GOAL]
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Angle.coe ∘ arg) ∘ Neg.neg) x = ↑(arg x) + ↑π
[PROOFSTEP]
exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
[GOAL]
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ↑π = ↑(arg 0) + ↑π
[PROOFSTEP]
simp
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
⊢ ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
[PROOFSTEP]
rw [ha]
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
⊢ ContinuousAt (fun z => ↑(arg z) + ↑π) (-x)
[PROOFSTEP]
push_neg at hs 
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ ContinuousAt (fun z => ↑(arg z) + ↑π) (-x)
[PROOFSTEP]
refine' (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl _))).add continuousAt_const
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < (-x).re
[PROOFSTEP]
rw [neg_re, neg_pos]
[GOAL]
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0
[PROOFSTEP]
exact hs.1.lt_of_ne fun h0 => h (ext_iff.2 ⟨h0, hs.2⟩)
