awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
neg : { re := 0, im := y : ℂ }.arg = I.arg
neg₁ : { re := 0, im := y : ℂ }.arg = ((↑y : ℂ) * I).arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg₂ : { re := 0, im := y : ℂ }.arg = { re := y * I.re, im := y * I.im }.arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
neg : { re := 0, im := y : ℂ }.arg = I.arg
neg₁ : { re := 0, im := y : ℂ }.arg = ((↑y : ℂ) * I).arg
neg₂ : { re := 0, im := y : ℂ }.arg = { re := y * I.re, im := y * I.im }.arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg₃ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * I.im }.arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
neg : { re := 0, im := y : ℂ }.arg = I.arg
neg₁ : { re := 0, im := y : ℂ }.arg = ((↑y : ℂ) * I).arg
neg₂ : { re := 0, im := y : ℂ }.arg = { re := y * I.re, im := y * I.im }.arg
neg₃ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * I.im }.arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg₄ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * 1 }.arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
neg : { re := 0, im := y : ℂ }.arg = I.arg
neg₁ : { re := 0, im := y : ℂ }.arg = ((↑y : ℂ) * I).arg
neg₂ : { re := 0, im := y : ℂ }.arg = { re := y * I.re, im := y * I.im }.arg
neg₃ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * I.im }.arg
neg₄ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * 1 }.arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg₅ : { re := 0, im := y : ℂ }.arg = { re := 0, im := y * 1 }.arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : 0 < y
neg : { re := 0, im := y : ℂ }.arg = I.arg
neg₁ : { re := 0, im := y : ℂ }.arg = ((↑y : ℂ) * I).arg
neg₂ : { re := 0, im := y : ℂ }.arg = { re := y * I.re, im := y * I.im }.arg
neg₃ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * I.im }.arg
neg₄ : { re := 0, im := y : ℂ }.arg = { re := y * 0, im := y * 1 }.arg
neg₅ : { re := 0, im := y : ℂ }.arg = { re := 0, im := y * 1 }.arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2
have neg₆ : { re := 0, im := y : ℂ }.arg = { re := 0, im := y }.arg
Tactic: rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
have pos : ∀ (h₀ : z = 0), z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
Tactic: by_cases h₀ : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
pos : ∀ (h₀ : z = 0), z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
have neg : ∀ (h₀ : ¬z = 0), z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
Tactic: by_cases h₀ : z = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
have neg : z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
neg : z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
have neg₁ : z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ z.re = 0 ∧ z.im < 0
have neg : ((↑‖z‖ : ℂ) * (cos (↑(-(π / 2)) : ℂ) + sin (↑(-(π / 2)) : ℂ) * I)).re = 0 ∧
  ((↑‖z‖ : ℂ) * (cos (↑(-(π / 2)) : ℂ) + sin (↑(-(π / 2)) : ℂ) * I)).im < 0
Tactic: rw [← norm_mul_cos_add_sin_mul_I z, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)
have neg : ∀ (x y : ℝ) (h₀ : ¬{ re := x, im := y : ℂ } = 0),
  { re := x, im := y : ℂ }.re = 0 ∧ { re := x, im := y : ℂ }.im < 0 → { re := x, im := y : ℂ }.arg = -(π / 2)
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: z, h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : y < 0
⊢ { re := 0, im := y : ℂ }.arg = -(π / 2)
have neg : ((↑0 : ℂ) + (↑y : ℂ) * I).arg = ((↑(-y) : ℂ) * -I).arg
Tactic: rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
⊢ z.arg = Real.arccos (z.re / ‖z‖)
have rw : z.arg = Real.arccos (Real.cos z.arg)
Tactic: rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
rw : z.arg = Real.arccos (Real.cos z.arg)
⊢ z.arg = Real.arccos (z.re / ‖z‖)
have rw₁ : z.arg = z.arg
Tactic: rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
z : ℂ
hz : z.im < 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)
have h₀ : z ≠ 0
Tactic: have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)
have hx₁ : 0 ≤ -z.arg
Tactic: rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
hx₁ : 0 ≤ -z.arg
⊢ z.arg = -Real.arccos (z.re / ‖z‖)
have hx₂ : -z.arg ≤ π
Tactic: rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = if x.arg = π then π else -x.arg
have simp_rw : (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
  else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
  if x.re < 0 ∧ x.im = 0 then π
  else
    -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, norm_conj, neg_div, neg_neg,
    Real.arcsin_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inl : ∀ (hr : x.re < 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.re 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
inl :
  ∀ (hr : x.re < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr : ∀ (hr : x.re = 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.re 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
inl :
  ∀ (hr : x.re < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
inr :
  ∀ (hr : x.re = 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr₁ : ∀ (hr : 0 < x.re),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.re 0 with (hr | hr | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : x.re < 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inl : ∀ (hi : x.im < 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : x.re < 0
inl :
  ∀ (hi : x.im < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inl₁ : ∀ (hi : x.im = 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : x.re < 0
inl :
  ∀ (hi : x.im < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
inl₁ :
  ∀ (hi : x.im = 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inl₂ : ∀ (hi : 0 < x.im),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : x.re = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr : ∀ (hi : x.im < 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : x.re = 0
inr :
  ∀ (hi : x.im < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr₁ : ∀ (hi : x.im = 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : x.re = 0
inr :
  ∀ (hi : x.im < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
inr₁ :
  ∀ (hi : x.im = 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr₂ : ∀ (hi : 0 < x.im),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : 0 < x.re
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr : ∀ (hi : x.im < 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : 0 < x.re
inr :
  ∀ (hi : x.im < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr₁ : ∀ (hi : x.im = 0),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
hr : 0 < x.re
inr :
  ∀ (hi : x.im < 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
inr₁ :
  ∀ (hi : x.im = 0),
    (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
      else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
      if x.re < 0 ∧ x.im = 0 then π
      else
        -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
          else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
have inr₂ : ∀ (hi : 0 < x.im),
  (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Tactic: rcases lt_trichotomy x.im 0 with (hi | hi | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ x⁻¹.arg = if x.arg = π then π else -x.arg
have rw : (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
  arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
Tactic: rw [← arg_conj, inv_def, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
have pos : ∀ (hx : x = 0),
  (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
pos :
  ∀ (hx : x = 0),
    (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
      arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
⊢ (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
have neg : ∀ (hx : ¬x = 0),
  (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ |x⁻¹.arg| = |x.arg|
have rw : |if x.arg = π then π else -x.arg| = |x.arg|
Tactic: rw [arg_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|
have pos : x.arg = π → |π| = |x.arg|
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
pos : x.arg = π → |π| = |x.arg|
⊢ |if x.arg = π then π else -x.arg| = |x.arg|
have neg : ¬x.arg = π → |(-x.arg)| = |x.arg|
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ ‖x‖ = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
have rw : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
Tactic: rw [norm_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
⊢ (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
have mp : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
x : ℂ
mp : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
⊢ (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
have mpr : (∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x) → ∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x
Tactic: constructor