awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
simp [hre, hre.le, hre.ne']

Premises used: LT.lt.le, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
⊢ z.arg < π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
rw [lt_iff_le_and_ne, arg_le_pi_div_two_iff, Ne, arg_eq_pi_div_two_iff]

Premises used: lt_iff_le_and_ne, Complex.arg_le_pi_div_two_iff, Ne, Complex.arg_eq_pi_div_two_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
inl : ∀ (hre : z.re < 0), (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
inr : ∀ (hre : z.re = 0), (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
inr₁ : ∀ (hre : 0 < z.re), (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
rcases lt_trichotomy z.re 0 with hre | hre | hre

Premises used: Complex.re, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
⊢ z ≠ 0

Tactic:
simp [Complex.ext_iff, hre.ne]

Premises used: Complex.ext_iff, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
⊢ z ≠ 0

Tactic:
have : z ≠ 0 := by simp [Complex.ext_iff, hre.ne]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
this : z ≠ 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre.ne, hre.not_ge, hre.not_gt, this]

Premises used: LT.lt.not_gt, LT.lt.not_ge, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re = 0
⊢ z = 0 ↔ z.im = 0

Tactic:
simp [Complex.ext_iff, hre]

Premises used: Complex.ext_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re = 0
⊢ z = 0 ↔ z.im = 0

Tactic:
have : z = 0 ↔ z.im = 0 := by simp [Complex.ext_iff, hre]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re = 0
this : z = 0 ↔ z.im = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre, this, or_comm, le_iff_eq_or_lt]

Premises used: le_iff_eq_or_lt, or_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre, hre.le, hre.ne']

Premises used: LT.lt.le, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : -(π / 2) ≤ z.arg ∧ z.arg ≤ π / 2 ↔ 0 ≤ z.re
rw₁ : -(π / 2) ≤ z.arg ∧ (0 ≤ z.re ∨ z.im < 0) ↔ 0 ≤ z.re
rw₂ : (0 ≤ z.re ∨ 0 ≤ z.im) ∧ (0 ≤ z.re ∨ z.im < 0) ↔ 0 ≤ z.re
rw₃ : 0 ≤ z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 0 ≤ z.re
rw₄ : 0 ≤ z.re ∨ 0 ≤ z.im ∧ ¬0 ≤ z.im ↔ 0 ≤ z.re
rw₅ : 0 ≤ z.re ∨ False ↔ 0 ≤ z.re
rw₆ rw₇ : 0 ≤ z.re ↔ 0 ≤ z.re
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re

Tactic:
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]

Premises used: not_le, Complex.arg_le_pi_div_two_iff, abs_le, and_not_self_iff, or_and_left, Complex.neg_pi_div_two_le_arg_iff, or_false
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
⊢ |z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0

Tactic:
rw [abs_lt, arg_lt_pi_div_two_iff, neg_pi_div_two_lt_arg_iff, ← or_and_left]

Premises used: Complex.neg_pi_div_two_lt_arg_iff, Complex.arg_lt_pi_div_two_iff, or_and_left, abs_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
inl : ∀ (hz : z = 0), 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
inr : ∀ (hz : z ≠ 0), 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
rcases eq_or_ne z 0 with hz | hz

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z = 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z ≠ 0
inr : 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ False) ↔ 0 < z.re ∨ False
inr₁ : 0 < z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 0 < z.re
inr₂ : 0 < z.re ∨ ¬z.im < 0 ∧ z.im < 0 ↔ 0 < z.re
inr₃ : 0 < z.re ∨ False ↔ 0 < z.re
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]

Premises used: not_lt, or_false, not_and_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
pos : ∀ (h : x.arg = π), (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
neg : ∀ (h : ¬x.arg = π), (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
⊢ (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)

Tactic:
by_cases h : arg x = π

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x.arg = π
⊢ (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)

Tactic:
simp [arg_conj, h]

Premises used: Complex.arg_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : ¬x.arg = π
⊢ (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)

Tactic:
simp [arg_conj, h]

Premises used: Complex.arg_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
pos : ∀ (h : x.arg = π), (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
neg : ∀ (h : ¬x.arg = π), (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
⊢ (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)

Tactic:
by_cases h : arg x = π

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x.arg = π
⊢ (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)

Tactic:
simp [arg_inv, h]

Premises used: Complex.arg_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : ¬x.arg = π
⊢ (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)

Tactic:
simp [arg_inv, h]

Premises used: Complex.arg_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : 0 < x.im
rw : -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π
⊢ (-x).arg = x.arg - π

Tactic:
rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]

Premises used: Iff.mpr, Left.neg_neg_iff, Complex.arg_of_im_pos, Complex.arg_of_im_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π

Tactic:
simp [neg_div, Real.arccos_neg]

Premises used: neg_div, Real.arccos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im < 0
rw : Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π
⊢ (-x).arg = x.arg + π

Tactic:
rw [arg_of_im_neg hi, arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)]

Premises used: Iff.mpr, Complex.arg_of_im_pos, Complex.arg_of_im_neg, Left.neg_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im < 0
⊢ Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π

Tactic:
simp [neg_div, Real.arccos_neg, add_comm, ← sub_eq_add_neg]

Premises used: neg_div, sub_eq_add_neg, Real.arccos_neg, add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
inl : ∀ (hi : x.im < 0), (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
inr : ∀ (hi : x.im = 0), (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
inr₁ : ∀ (hi : 0 < x.im), (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
rcases lt_trichotomy x.im 0 with (hi | hi | hi)

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im < 0
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
simp [hi, hi.ne, hi.not_gt, arg_neg_eq_arg_add_pi_of_im_neg, sub_eq_add_neg, ←
      add_eq_zero_iff_eq_neg, Real.pi_ne_zero]

Premises used: sub_eq_add_neg, add_eq_zero_iff_eq_neg, Complex.arg_neg_eq_arg_add_pi_of_im_neg, LT.lt.not_gt, Real.pi_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
inr : (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
rw [(ext rfl hi : x = x.re)]

Premises used: Complex.ext, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
inr :
  ∀ (hr : x.re < 0),
    (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
inr₁ :
  ∀ (hr : x.re = 0),
    (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
inr₂ :
  ∀ (hr : 0 < x.re),
    (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Premises used: Complex.re, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : x.re < 0
inr : 0 = π - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0

Tactic:
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]

Premises used: Iff.mpr, Complex.arg_ofReal_of_nonneg, Complex.ofReal_neg, LT.lt.le, Left.neg_pos_iff, Complex.arg_ofReal_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0

Tactic:
simp [hr, Real.pi_ne_zero]

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : 0 < x.re
inr : π = 0 - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]

Premises used: Iff.mpr, Left.neg_neg_iff, Complex.arg_ofReal_of_nonneg, Complex.ofReal_neg, LT.lt.le, Complex.arg_ofReal_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0

Tactic:
simp [hr.not_gt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]

Premises used: add_eq_zero_iff_eq_neg, LT.lt.not_gt, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
simp [hi, arg_neg_eq_arg_sub_pi_of_im_pos]

Premises used: Complex.arg_neg_eq_arg_sub_pi_of_im_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
inl : ∀ (hi : x.im < 0), (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
inr : ∀ (hi : x.im = 0), (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
inr₁ : ∀ (hi : 0 < x.im), (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
rcases lt_trichotomy x.im 0 with (hi | hi | hi)

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im < 0
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
simp [hi, arg_neg_eq_arg_add_pi_of_im_neg]

Premises used: Complex.arg_neg_eq_arg_add_pi_of_im_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
inr : (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
rw [(ext rfl hi : x = x.re)]

Premises used: Complex.ext, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
inr :
  ∀ (hr : x.re < 0),
    (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
inr₁ :
  ∀ (hr : x.re = 0),
    (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
inr₂ :
  ∀ (hr : 0 < x.re),
    (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Premises used: Complex.re, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : x.re < 0
inr : 0 = π + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re

Tactic:
rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le]

Premises used: Iff.mpr, Complex.arg_ofReal_of_nonneg, Complex.ofReal_neg, LT.lt.le, Left.neg_pos_iff, Complex.arg_ofReal_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ 0 = π + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re

Tactic:
simp [hr.not_gt, ← two_mul, Real.pi_ne_zero]

Premises used: two_mul, LT.lt.not_gt, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re

Tactic:
simp [hr, Real.pi_ne_zero.symm]

Premises used: Ne.symm, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : 0 < x.re
inr : π = 0 + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re

Tactic:
rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]

Premises used: Iff.mpr, Left.neg_neg_iff, Complex.arg_ofReal_of_nonneg, Complex.ofReal_neg, LT.lt.le, Complex.arg_ofReal_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ π = 0 + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
simp [hi, hi.ne.symm, hi.not_gt, arg_neg_eq_arg_sub_pi_of_im_pos, sub_eq_add_neg, ←
      add_eq_zero_iff_neg_eq, Real.pi_ne_zero]

Premises used: Complex.arg_neg_eq_arg_sub_pi_of_im_pos, sub_eq_add_neg, Ne.symm, add_eq_zero_iff_neg_eq, LT.lt.not_gt, Real.pi_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
inl : ∀ (hi : x.im < 0), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
inr : ∀ (hi : x.im = 0), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
inr₁ : ∀ (hi : 0 < x.im), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
rcases lt_trichotomy x.im 0 with (hi | hi | hi)

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im < 0
inl : (↑(x.arg + π) : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
inl₁ inl₂ : (↑x.arg : Real.Angle) + (↑π : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]

Premises used: Real.Angle.coe_add, Complex.arg_neg_eq_arg_add_pi_of_im_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
rw [(ext rfl hi : x = x.re)]

Premises used: Complex.ext, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
inr : ∀ (hr : x.re < 0), (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
inr₁ : ∀ (hr : x.re = 0), (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
inr₂ : ∀ (hr : 0 < x.re), (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Premises used: Complex.re, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑π : Real.Angle) + (↑π : Real.Angle)
inr₁ : (↑(↑(-x.re) : ℂ).arg : Real.Angle) = (↑π : Real.Angle) + (↑π : Real.Angle)
inr₂ : (↑0 : Real.Angle) = (↑π : Real.Angle) + (↑π : Real.Angle)
inr₃ : (↑0 : Real.Angle) = (↑(π + π) : Real.Angle)
inr₄ : (↑0 : Real.Angle) = (↑(2 * π) : Real.Angle)
inr₅ : (↑0 : Real.Angle) = 0
inr₆ inr₇ : Eq (α := Real.Angle) 0 0
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
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]

Premises used: Iff.mpr, Complex.arg_ofReal_of_nonneg, Real.Angle.coe_add, Complex.ofReal_neg, two_mul, LT.lt.le, Left.neg_pos_iff, Real.Angle.coe_two_pi, Complex.arg_ofReal_of_neg, Real.Angle.coe_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
False.elim (hx (ext hr hi))

Premises used: False.elim, Complex.ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
exact False.elim (hx (ext hr hi))

Premises used: False.elim, Complex.ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑0 : Real.Angle) + (↑π : Real.Angle)
inr₁ : (↑(↑(-x.re) : ℂ).arg : Real.Angle) = (↑0 : Real.Angle) + (↑π : Real.Angle)
inr₂ : (↑π : Real.Angle) = (↑0 : Real.Angle) + (↑π : Real.Angle)
inr₃ : (↑π : Real.Angle) = 0 + (↑π : Real.Angle)
inr₄ inr₅ : (↑π : Real.Angle) = (↑π : Real.Angle)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
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]

Premises used: Iff.mpr, Left.neg_neg_iff, Complex.arg_ofReal_of_nonneg, Complex.ofReal_neg, LT.lt.le, zero_add, Complex.arg_ofReal_of_neg, Real.Angle.coe_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
inr : (↑(x.arg - π) : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
inr₁ : (↑x.arg : Real.Angle) - (↑π : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
inr₂ inr₃ : (↑x.arg : Real.Angle) + (↑π : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)

Tactic:
rw [arg_neg_eq_arg_sub_pi_of_im_pos hi, Real.Angle.coe_sub, Real.Angle.sub_coe_pi_eq_add_coe_pi]

Premises used: Complex.arg_neg_eq_arg_sub_pi_of_im_pos, Real.Angle.sub_coe_pi_eq_add_coe_pi, Real.Angle.coe_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
rw : (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
rw₁ : (cexp ((↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
rw₂ rw₃ : toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
rw [arg_real_mul _ hr, ← exp_mul_I, arg_exp_mul_I]

Premises used: Complex.arg_exp_mul_I, Complex.arg_real_mul, Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
rw₂ rw₃ : toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]

Premises used: Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod, Complex.ofReal_one, zero_lt_one, HAdd.hAdd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
rw : (↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) : ℝ) * (2 * π) = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)

Tactic:
rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor,
    zsmul_eq_mul]

Premises used: zsmul_eq_mul, Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod, toIocMod_sub_self, toIocDiv_eq_neg_floor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) : ℝ) * (2 * π) = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
rw₂ rw₃ : 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ) = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]

Premises used: Complex.ofReal_one, zero_lt_one, HAdd.hAdd, Complex.arg_mul_cos_add_sin_mul_I_sub, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : Real.Angle
h :
  ∀ (θ : ℝ),
    (↑((↑r : ℂ) * ((↑(↑θ : Real.Angle).cos : ℂ) + (↑(↑θ : Real.Angle).sin : ℂ) * I)).arg : Real.Angle) =
      (↑θ : Real.Angle)
⊢ (↑((↑r : ℂ) * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ

Tactic:
induction θ using Real.Angle.induction_on with | _ θ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑((↑r : ℂ) * ((↑(↑θ : Real.Angle).cos : ℂ) + (↑(↑θ : Real.Angle).sin : ℂ) * I)).arg : Real.Angle) = (↑θ : Real.Angle)

Tactic:
simp [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr]

Premises used: Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : Real.Angle
rw : (↑(1 * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
rw₁ : (↑((↑1 : ℂ) * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
rw₂ rw₃ : θ = θ
⊢ (↑((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I).arg : Real.Angle) = θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]

Premises used: Complex.arg_mul_cos_add_sin_mul_I_coe_angle, Complex.ofReal_one, zero_lt_one, HAdd.hAdd, one_mul