awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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‖) - π
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‖) - π
⊢ (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)

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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‖) - π
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‖) - π
⊢ (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)

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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‖) - π
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‖) - π
⊢ (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)

Premises used: Complex.im, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : x.re < 0
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:
simp [hr, hr.not_ge, hi.le, hi.ne, not_le.2 hi, add_comm]

Premises used: not_le, Iff.mpr, LT.lt.le, add_comm, LT.lt.not_ge, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : x.re < 0
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:
simp [hr, hr.not_ge, hi]

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : x.re < 0
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:
simp [hr, hr.not_ge, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]

Premises used: not_le, Iff.mpr, sub_eq_neg_add, LT.lt.le, Ne.symm, LT.lt.not_ge, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : x.re = 0
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:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : x.re = 0
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:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : x.re = 0
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:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : 0 < x.re
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:
simp [hr.le, hi.ne]

Premises used: LT.lt.le, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : 0 < x.re
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:
simp [hr.le, hr.le.not_gt]

Premises used: LT.lt.le, LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hr : 0 < x.re
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:
simp [hr.le, hr.le.not_gt]

Premises used: LT.lt.le, LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
rw :
  (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
⊢ x⁻¹.arg = if x.arg = π then π else -x.arg

Tactic:
rw [← arg_conj, inv_def, mul_comm]

Premises used: Complex.inv_def, Complex.arg_conj, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
pos :
  ∀ (hx : x = 0),
    (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
      arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)
neg :
  ∀ (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)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x = 0
⊢ (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : ¬x = 0
⊢ LT.lt (α := ℝ) (0 : ℝ) (((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℝ)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : ¬x = 0
⊢ (HMul.hMul (β := ℂ) (↑((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ)).arg =
    arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x)

Tactic:
exact arg_real_mul (conj x) (by simp [hx])

Premises used: Complex.arg_real_mul, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
rw : |if x.arg = π then π else -x.arg| = |x.arg|
⊢ |x⁻¹.arg| = |x.arg|

Tactic:
rw [arg_inv]

Premises used: Complex.arg_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
pos : x.arg = π → |π| = |x.arg|
neg : ¬x.arg = π → |(-x.arg)| = |x.arg|
⊢ |if x.arg = π then π else -x.arg| = |x.arg|

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x.arg = π
⊢ |π| = |x.arg|

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : ¬x.arg = π
⊢ |(-x.arg)| = |x.arg|

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
rw : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
⊢ ‖x‖ = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x

Tactic:
rw [norm_eq_one_iff]

Premises used: Complex.norm_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
mp : (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x
mpr : (∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x) → ∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x
⊢ (∃ (θ : ℝ), cexp ((↑θ : ℂ) * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp ((↑θ : ℂ) * I) = x

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp ((↑θ_1 : ℂ) * I) = cexp ((↑θ : ℂ) * I)

Tactic:
⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩

Premises used: Real.pi, two_pos, Real.pi_pos, mul_pos, And.intro, toIocMod, Exists.intro, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
mp : toIocMod (p := 2 * π) ⋯ (-π) θ ∈ Ioc (-π) π
mp₁ : cexp ((↑(toIocMod (p := 2 * π) ⋯ (-π) θ) : ℂ) * I) = cexp ((↑θ : ℂ) * I)
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp ((↑θ_1 : ℂ) * I) = cexp ((↑θ : ℂ) * I)

Tactic:
refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
⊢ toIocMod (p := 2 * π) ⋯ (-π) θ ∈ Ioc (-π) (-π + 2 * π)

Tactic:
toIocMod_mem_Ioc _ _ _

Premises used: toIocMod_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
h : π = -π + 2 * π
⊢ toIocMod (p := 2 * π) ⋯ (-π) θ ∈ Ioc (-π) π

Tactic:
convert! toIocMod_mem_Ioc _ _ _

Premises used: toIocMod_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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)
mp₅ mp₆ : cexp ((↑θ : ℂ) * I) = cexp ((↑θ : ℂ) * I)
⊢ cexp ((↑(toIocMod (p := 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]

Premises used: eq_sub_of_add_eq, toIocMod_add_toIocDiv_zsmul, Function.Periodic.sub_zsmul_eq, Complex.ofReal_zsmul, Complex.ofReal_sub, Complex.ofReal_ofNat, Complex.exp_mul_I_periodic, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
left : θ ∈ Ioc (-π) π
⊢ ∃ (θ_1 : ℝ), cexp ((↑θ_1 : ℂ) * I) = cexp ((↑θ : ℂ) * I)

Tactic:
⟨θ, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
left : θ ∈ Ioc (-π) π
⊢ ∃ (θ_1 : ℝ), cexp ((↑θ_1 : ℂ) * I) = cexp ((↑θ : ℂ) * I)

Tactic:
exact ⟨θ, rfl⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) ((fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) '' Ioc (-π) π) x ↔
      Membership.mem (γ := Set ℂ) (sphere 0 1) x
⊢ Eq (α := Set ℂ) ((fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) '' Ioc (-π) π) (sphere 0 1)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
⊢ Membership.mem (γ := Set ℂ) ((fun (θ : ℝ) ↦ cexp ((↑θ : ℂ) * I)) '' Ioc (-π) π) x ↔
    Membership.mem (γ := Set ℂ) (sphere 0 1) x

Tactic:
simpa using norm_eq_one_iff'.symm

Premises used: Complex.norm_eq_one_iff', Iff.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
inl : ∀ (hre : 0 ≤ z.re), z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
inr : ∀ (hre : z.re < 0), z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
rcases le_or_gt 0 (re z) with hre | hre

Premises used: Complex.re, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : 0 ≤ z.re
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or]

Premises used: Complex.arg_of_re_nonneg, true_or, Real.arcsin_le_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
inr : z.arg ≤ π / 2 ↔ z.im < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
simp only [hre.not_ge, false_or]

Premises used: false_or, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
inr : ∀ (him : 0 ≤ z.im), z.arg ≤ π / 2 ↔ z.im < 0
inr₁ : ∀ (him : z.im < 0), z.arg ≤ π / 2 ↔ z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
rcases le_or_gt 0 (im z) with him | him

Premises used: Complex.im, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
inr : z.arg ≤ π / 2 ↔ False
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
simp only [him.not_gt]

Premises used: LE.le.not_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
inr : z.re ≠ 0
inr₁ : 0 < ‖z‖
⊢ z.arg ≤ π / 2 ↔ False

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]

Premises used: not_le, neg_lt_neg_iff, neg_div, iff_false, Complex.arg_of_re_neg_of_im_nonneg, Complex.abs_im_lt_norm, Real.neg_pi_div_two_lt_arcsin, half_sub, div_lt_one, abs_of_nonneg, sub_lt_iff_lt_add, Complex.neg_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

Tactic:
hre.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖

Tactic:
norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne

Premises used: Iff.mpr, norm_pos_iff, ne_of_apply_ne, Complex.re, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

Tactic:
exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

Premises used: Iff.mpr, norm_pos_iff, ne_of_apply_ne, Complex.re, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
inr : z.arg ≤ π / 2 ↔ True
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
simp only [him]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
inr : Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2
⊢ z.arg ≤ π / 2 ↔ True

Tactic:
rw [iff_true, arg_of_re_neg_of_im_neg hre him]

Premises used: iff_true, Complex.arg_of_re_neg_of_im_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2

Tactic:
(sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)

Premises used: Real.arcsin_le_pi_div_two, Real.pi_pos, LT.lt.le, sub_le_self, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2

Tactic:
exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)

Premises used: Real.arcsin_le_pi_div_two, Real.pi_pos, LT.lt.le, sub_le_self, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
inl : ∀ (hre : 0 ≤ z.re), -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
inr : ∀ (hre : z.re < 0), -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
rcases le_or_gt 0 (re z) with hre | hre

Premises used: Complex.re, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
simp only [hre, arg_of_re_nonneg hre, Real.neg_pi_div_two_le_arcsin, true_or]

Premises used: Complex.arg_of_re_nonneg, true_or, Real.neg_pi_div_two_le_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
inr : -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
simp only [hre.not_ge, false_or]

Premises used: false_or, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
inr : ∀ (him : 0 ≤ z.im), -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
inr₁ : ∀ (him : z.im < 0), -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
rcases le_or_gt 0 (im z) with him | him

Premises used: Complex.im, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
inr : -(π / 2) ≤ z.arg ↔ True
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
simp only [him]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
inr : -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π
⊢ -(π / 2) ≤ z.arg ↔ True

Tactic:
rw [iff_true, arg_of_re_neg_of_im_nonneg hre him]

Premises used: Complex.arg_of_re_neg_of_im_nonneg, iff_true
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
(Real.neg_pi_div_two_le_arcsin _).trans (le_add_of_nonneg_right Real.pi_pos.le)

Premises used: Real.pi_pos, LT.lt.le, le_add_of_nonneg_right, Real.neg_pi_div_two_le_arcsin, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
exact (Real.neg_pi_div_two_le_arcsin _).trans (le_add_of_nonneg_right Real.pi_pos.le)

Premises used: Real.pi_pos, LT.lt.le, le_add_of_nonneg_right, Real.neg_pi_div_two_le_arcsin, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
inr : -(π / 2) ≤ z.arg ↔ False
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
simp only [him.not_ge]

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
inr : z.re ≠ 0
inr₁ : 0 < ‖z‖
⊢ -(π / 2) ≤ z.arg ↔ False

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]

Premises used: not_le, iff_false, abs_of_neg, sub_eq_add_neg, Complex.arg_of_re_neg_of_im_neg, sub_lt_iff_lt_add', Complex.abs_im_lt_norm, div_lt_one, Real.arcsin_lt_pi_div_two, sub_half, Complex.neg_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

Tactic:
hre.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖

Tactic:
norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne

Premises used: Iff.mpr, norm_pos_iff, ne_of_apply_ne, Complex.re, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

Tactic:
exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

Premises used: Iff.mpr, norm_pos_iff, ne_of_apply_ne, Complex.re, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
⊢ -(π / 2) < z.arg ↔ 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]

Premises used: lt_iff_le_and_ne, Ne, ne_comm, Complex.neg_pi_div_two_le_arg_iff, Complex.arg_eq_neg_pi_div_two_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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
inr₁ : ∀ (hre : 0 < z.re), (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

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
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

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

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
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
simp [hre]