awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
have inr₂ : ∀ (hr : 0 < x.re),
  (-(↑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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
have inr : 0 = π - π ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
have inr : π = 0 - π ↔ 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
have inl : ∀ (hi : x.im < 0), (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
inl : ∀ (hi : x.im < 0), (-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
have inr : ∀ (hi : x.im = 0), (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
have inr₁ : ∀ (hi : 0 < x.im), (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hi : x.im = 0
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
have inr : (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
Tactic: rw [(ext rfl hi : x = x.re)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hi : x.im = 0
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
have inr : ∀ (hr : x.re < 0),
  (-(↑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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
have inr₁ : ∀ (hr : x.re = 0),
  (-(↑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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
have inr₂ : ∀ (hr : 0 < x.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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
have inr : 0 = π + π ↔ (↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg + π ↔ (↑x.re : ℂ).im < 0 ∨ (↑x.re : ℂ).im = 0 ∧ 0 < (↑x.re : ℂ).re
have inr : π = 0 + π ↔ (↑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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inl : ∀ (hi : x.im < 0), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
inl : ∀ (hi : x.im < 0), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inr : ∀ (hi : x.im = 0), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inr₁ : ∀ (hi : 0 < x.im), (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inl : (↑(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im < 0
inl : (↑(x.arg + π) : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inl₁ : (↑x.arg : Real.Angle) + (↑π : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rw [arg_neg_eq_arg_add_pi_of_im_neg hi, Real.Angle.coe_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rw [(ext rfl hi : x = x.re)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr : ∀ (hr : x.re < 0), (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rcases lt_trichotomy x.re 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₁ : ∀ (hr : x.re = 0), (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rcases lt_trichotomy x.re 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₂ : ∀ (hr : 0 < x.re), (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
Tactic: rcases lt_trichotomy x.re 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
have inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑π : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₁ : (↑(↑(-x.re) : ℂ).arg : Real.Angle) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₂ : (↑0 : Real.Angle) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₃ : (↑0 : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₄ : (↑0 : Real.Angle) = (↑(2 * π) : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₅ : (↑0 : Real.Angle) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₆ : Eq (α := Real.Angle) 0 0
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑0 : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
inr : (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑0 : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₁ : (↑(↑(-x.re) : ℂ).arg : Real.Angle) = (↑0 : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₂ : (↑π : Real.Angle) = (↑0 : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₃ : (↑π : Real.Angle) = 0 + (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-(↑x.re : ℂ)).arg : Real.Angle) = (↑(↑x.re : ℂ).arg : Real.Angle) + (↑π : Real.Angle)
have inr₄ : (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inr : (↑(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
inr : (↑(x.arg - π) : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inr₁ : (↑x.arg : Real.Angle) - (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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)
⊢ (↑(-x).arg : Real.Angle) = (↑x.arg : Real.Angle) + (↑π : Real.Angle)
have inr₂ : (↑x.arg : Real.Angle) + (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
have rw : (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
Tactic: rw [arg_real_mul _ hr, ← exp_mul_I, arg_exp_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
rw : (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
have rw₁ : (cexp ((↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
Tactic: rw [arg_real_mul _ hr, ← exp_mul_I, arg_exp_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
rw : (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
rw₁ : (cexp ((↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
have rw₂ : toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ
Tactic: rw [arg_real_mul _ hr, ← exp_mul_I, arg_exp_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
have rw : (1 * (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
have rw₁ : ((↑1 : ℂ) * (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = toIocMod Real.two_pi_pos (-π) θ
have rw₂ : toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
have rw : (↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) : ℝ) * (2 * π) = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
Tactic: rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor,
    zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
have rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
have rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg - θ = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
have rw₂ : 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ) = 2 * π * (↑⌊(π - θ) / (2 * π)⌋ : ℝ)
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_sub zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : Real.Angle
⊢ (↑((↑r : ℂ) * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
have h : ∀ (θ : ℝ),
  (↑((↑r : ℂ) * ((↑(↑θ : Real.Angle).cos : ℂ) + (↑(↑θ : Real.Angle).sin : ℂ) * I)).arg : Real.Angle) = (↑θ : Real.Angle)
Tactic: induction θ using Real.Angle.induction_on with | _ θ
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : Real.Angle
⊢ (↑((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I).arg : Real.Angle) = θ
have rw : (↑(1 * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : Real.Angle
rw : (↑(1 * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
⊢ (↑((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I).arg : Real.Angle) = θ
have rw₁ : (↑((↑1 : ℂ) * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : Real.Angle
rw : (↑(1 * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
rw₁ : (↑((↑1 : ℂ) * ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)).arg : Real.Angle) = θ
⊢ (↑((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I).arg : Real.Angle) = θ
have rw₂ : θ = θ
Tactic: rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]