awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp ((↑θ_1 : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp : toIocMod (p := 2 * π) sorry (-π) θ ∈ Ioc (-π) π
Tactic: refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
mp : toIocMod (p := 2 * π) ⋯ (-π) θ ∈ Ioc (-π) π
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp ((↑θ_1 : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp₁ : cexp ((↑(toIocMod (p := 2 * π) sorry (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
Tactic: refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
⊢ toIocMod (p := 2 * π) ⋯ (-π) θ ∈ Ioc (-π) π
have h : π = -π + 2 * π
Tactic: convert! toIocMod_mem_Ioc _ _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
⊢ cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp : cexp ((↑(θ - toIocDiv (p := 2 * π) sorry (-π) θ • (2 * π)) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
Tactic: rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
mp : cexp ((↑(θ - toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
⊢ cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp₁ : cexp (((↑θ : ℂ) - (↑(toIocDiv (p := 2 * π) sorry (-π) θ • (2 * π)) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
Tactic: rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
mp : cexp ((↑(θ - toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
mp₁ : cexp (((↑θ : ℂ) - (↑(toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
⊢ cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp₂ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) sorry (-π) θ • (↑(2 * π) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
Tactic: rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
mp : cexp ((↑(θ - toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
mp₁ : cexp (((↑θ : ℂ) - (↑(toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
mp₂ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) ⋯ (-π) θ • (↑(2 * π) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
⊢ cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp₃ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) sorry (-π) θ • ((↑2 : ℂ) * (↑π : ℂ))) * I) = cexp ((↑θ : ℂ) * I)
Tactic: rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
mp : cexp ((↑(θ - toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
mp₁ : cexp (((↑θ : ℂ) - (↑(toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
mp₂ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) ⋯ (-π) θ • (↑(2 * π) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
mp₃ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) ⋯ (-π) θ • ((↑2 : ℂ) * (↑π : ℂ))) * I) = cexp ((↑θ : ℂ) * I)
⊢ cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp₄ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) sorry (-π) θ • (2 * (↑π : ℂ))) * I) = cexp ((↑θ : ℂ) * I)
Tactic: rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
θ : ℝ
mp : cexp ((↑(θ - toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
mp₁ : cexp (((↑θ : ℂ) - (↑(toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * π)) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
mp₂ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) ⋯ (-π) θ • (↑(2 * π) : ℂ)) * I) = cexp ((↑θ : ℂ) * I)
mp₃ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) ⋯ (-π) θ • ((↑2 : ℂ) * (↑π : ℂ))) * I) = cexp ((↑θ : ℂ) * I)
mp₄ : cexp (((↑θ : ℂ) - toIocDiv (p := 2 * π) ⋯ (-π) θ • (2 * (↑π : ℂ))) * I) = cexp ((↑θ : ℂ) * I)
⊢ cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
have mp₅ : cexp ((↑θ : ℂ) * I) = cexp ((↑θ : ℂ) * I)
Tactic: rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
⊢ Eq (α := Set ℂ) ((fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) '' Ioc (-π) π) (sphere 0 1)
have h : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) ((fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) '' Ioc (-π) π) x ↔
    Membership.mem (γ := Set ℂ) (sphere 0 1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
have inl : ∀ (hre : 0 ≤ z.re), z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
Tactic: rcases le_or_gt 0 (re z) with hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
inl : ∀ (hre : 0 ≤ z.re), z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
have inr : ∀ (hre : z.re < 0), z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
Tactic: rcases le_or_gt 0 (re z) with hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
have inr : z.arg ≤ π / 2 ↔ z.im < 0
Tactic: simp only [hre.not_ge, false_or]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0
have inr : ∀ (him : 0 ≤ z.im), z.arg ≤ π / 2 ↔ z.im < 0
Tactic: rcases le_or_gt 0 (im z) with him | him
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
inr : ∀ (him : 0 ≤ z.im), z.arg ≤ π / 2 ↔ z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0
have inr₁ : ∀ (him : z.im < 0), z.arg ≤ π / 2 ↔ z.im < 0
Tactic: rcases le_or_gt 0 (im z) with him | him
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ z.im < 0
have inr : z.arg ≤ π / 2 ↔ False
Tactic: simp only [him.not_gt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ False
have inr : z.re ≠ 0
Tactic: rw [iff_false, 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, ←
      abs_of_nonneg him, abs_im_lt_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
inr : z.re ≠ 0
⊢ z.arg ≤ π / 2 ↔ False
have inr₁ : 0 < ‖z‖
Tactic: rw [iff_false, 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, ←
      abs_of_nonneg him, abs_im_lt_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0
have inr : z.arg ≤ π / 2 ↔ True
Tactic: simp only [him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ True
have inr : Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2
Tactic: rw [iff_true, arg_of_re_neg_of_im_neg hre him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
have inl : ∀ (hre : 0 ≤ z.re), -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
Tactic: rcases le_or_gt 0 (re z) with hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
inl : ∀ (hre : 0 ≤ z.re), -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
have inr : ∀ (hre : z.re < 0), -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
Tactic: rcases le_or_gt 0 (re z) with hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
have inr : -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
Tactic: simp only [hre.not_ge, false_or]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
have inr : ∀ (him : 0 ≤ z.im), -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
Tactic: rcases le_or_gt 0 (im z) with him | him
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
inr : ∀ (him : 0 ≤ z.im), -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
have inr₁ : ∀ (him : z.im < 0), -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
Tactic: rcases le_or_gt 0 (im z) with him | him
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
have inr : -(π / 2) ≤ z.arg ↔ True
Tactic: simp only [him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ True
have inr : -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π
Tactic: rw [iff_true, arg_of_re_neg_of_im_nonneg hre him]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
have inr : -(π / 2) ≤ z.arg ↔ False
Tactic: simp only [him.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ False
have inr : z.re ≠ 0
Tactic: rw [iff_false, 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_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
inr : z.re ≠ 0
⊢ -(π / 2) ≤ z.arg ↔ False
have inr₁ : 0 < ‖z‖
Tactic: rw [iff_false, 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_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ -(π / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im
have rw : (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
Tactic: rw [lt_iff_le_and_ne, neg_pi_div_two_le_arg_iff, ne_comm, Ne, arg_eq_neg_pi_div_two_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
have inl : ∀ (hre : z.re < 0), (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
Tactic: rcases lt_trichotomy z.re 0 with hre | hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
inl : ∀ (hre : z.re < 0), (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
have inr : ∀ (hre : z.re = 0), (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
Tactic: rcases lt_trichotomy z.re 0 with hre | hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
inl : ∀ (hre : z.re < 0), (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
inr : ∀ (hre : z.re = 0), (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
have inr₁ : ∀ (hre : 0 < z.re), (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
Tactic: rcases lt_trichotomy z.re 0 with hre | hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg < π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
have rw : (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
have 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
Tactic: rcases lt_trichotomy z.re 0 with hre | hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
have 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
Tactic: rcases lt_trichotomy z.re 0 with hre | hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
have 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
Tactic: rcases lt_trichotomy z.re 0 with hre | hre | hre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hre : z.re < 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
have this : z ≠ 0
Tactic: have : z ≠ 0 := by simp [Complex.ext_iff, hre.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
have this : z = 0 ↔ z.im = 0
Tactic: have : z = 0 ↔ z.im = 0 := by simp [Complex.ext_iff, hre]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw : -(π / 2) ≤ z.arg ∧ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
rw : -(π / 2) ≤ z.arg ∧ z.arg ≤ π / 2 ↔ 0 ≤ z.re
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw₁ : -(π / 2) ≤ z.arg ∧ (0 ≤ z.re ∨ z.im < 0) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw₂ : (0 ≤ z.re ∨ 0 ≤ z.im) ∧ (0 ≤ z.re ∨ z.im < 0) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw₃ : 0 ≤ z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw₄ : 0 ≤ z.re ∨ 0 ≤ z.im ∧ ¬0 ≤ z.im ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw₅ : 0 ≤ z.re ∨ False ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ |z.arg| ≤ π / 2 ↔ 0 ≤ z.re
have rw₆ : 0 ≤ z.re ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ |z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0
have rw : 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
have inl : ∀ (hz : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
inl : ∀ (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
have inr : ∀ (hz : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
have inr : 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ False) ↔ 0 < z.re ∨ False
Tactic: simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : z ≠ 0
inr : 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ False) ↔ 0 < z.re ∨ False
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
have inr₁ : 0 < z.re ∨ 0 ≤ z.im ∧ z.im < 0 ↔ 0 < z.re
Tactic: simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
have inr₂ : 0 < z.re ∨ ¬z.im < 0 ∧ z.im < 0 ↔ 0 < z.re
Tactic: simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
have inr₃ : 0 < z.re ∨ False ↔ 0 < z.re
Tactic: simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
have pos : ∀ (h : x.arg = π), (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
Tactic: by_cases h : arg x = π
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
pos : ∀ (h : x.arg = π), (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
⊢ (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
have neg : ∀ (h : ¬x.arg = π), (↑(arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : Real.Angle) = -(↑x.arg : Real.Angle)
Tactic: by_cases h : arg x = π
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
have pos : ∀ (h : x.arg = π), (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
Tactic: by_cases h : arg x = π
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
pos : ∀ (h : x.arg = π), (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
⊢ (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
have neg : ∀ (h : ¬x.arg = π), (↑x⁻¹.arg : Real.Angle) = -(↑x.arg : Real.Angle)
Tactic: by_cases h : arg x = π
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg - π
have rw : -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π
Tactic: rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hi : x.im < 0
⊢ (-x).arg = x.arg + π
have rw : Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π
Tactic: rw [arg_of_im_neg hi, arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
have inl : ∀ (hi : x.im < 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
inl : ∀ (hi : x.im < 0), (-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
have inr : ∀ (hi : x.im = 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
have inr₁ : ∀ (hi : 0 < x.im), (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
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 - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
have inr : (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
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 - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
have inr : ∀ (hr : x.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)
-- 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
⊢ (-(↑x.re : ℂ)).arg = (↑x.re : ℂ).arg - π ↔ 0 < (↑x.re : ℂ).im ∨ (↑x.re : ℂ).im = 0 ∧ (↑x.re : ℂ).re < 0
have inr₁ : ∀ (hr : x.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)