awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ range arg = Ioc (-π) π

Tactic:
(Set.range_subset_iff.2 arg_mem_Ioc).antisymm fun _ hx => ⟨_, arg_cos_add_sin_mul_I hx⟩

Premises used: Iff.mpr, HMul.hMul, Complex.cos, Complex.arg_cos_add_sin_mul_I, Complex.sin, Complex.arg_mem_Ioc, Complex.ofReal, HAdd.hAdd, HasSubset.Subset.antisymm, Exists.intro, Set.range_subset_iff, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
⊢ x.arg ≤ π

Tactic:
(arg_mem_Ioc x).2

Premises used: Complex.arg_mem_Ioc, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
⊢ -π < x.arg

Tactic:
(arg_mem_Ioc x).1

Premises used: Complex.arg_mem_Ioc, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
⊢ x.arg < y.arg + 2 * π

Tactic:
grind [arg_le_pi x, neg_pi_lt_arg y]

Premises used: Complex.arg_le_pi, Complex.neg_pi_lt_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
⊢ |x.arg - y.arg| < 2 * π

Tactic:
grind [arg_lt_arg_add_two_pi x y, arg_lt_arg_add_two_pi y x]

Premises used: Complex.arg_lt_arg_add_two_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ |z.arg| ≤ π

Tactic:
abs_le.2 ⟨(neg_pi_lt_arg z).le, arg_le_pi z⟩

Premises used: Iff.mpr, Complex.arg_le_pi, abs_le, LT.lt.le, Complex.neg_pi_lt_arg, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
inl : 0 ≤ arg 0 ↔ 0 ≤ im 0
inr : ∀ (h₀ : z ≠ 0), 0 ≤ z.arg ↔ 0 ≤ z.im
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ 0 ≤ arg 0 ↔ 0 ≤ im 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z ≠ 0
contrapose! : z.arg < 0 → Real.sin z.arg < 0
⊢ 0 ≤ Real.sin z.arg → 0 ≤ z.arg

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z ≠ 0
h : z.arg < 0
⊢ Real.sin z.arg < 0

Tactic:
Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)

Premises used: Complex.neg_pi_lt_arg, Real.sin_neg_of_neg_of_neg_pi_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z ≠ 0
h : z.arg < 0
⊢ Real.sin z.arg < 0

Tactic:
exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)

Premises used: Complex.neg_pi_lt_arg, Real.sin_neg_of_neg_of_neg_pi_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z ≠ 0
rw : 0 ≤ z.im / ‖z‖ ↔ 0 ≤ z.im
rw₁ : 0 * ‖z‖ ≤ z.im ↔ 0 ≤ z.im
rw₂ rw₃ : 0 ≤ z.im ↔ 0 ≤ z.im
⊢ 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im

Tactic:
rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]

Premises used: Iff.mpr, norm_pos_iff, MulZeroClass.zero_mul, le_div_iff₀, Complex.sin_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z ≠ 0
arg : 0 ≤ Real.sin z.arg ↔ 0 ≤ z.im
⊢ 0 ≤ z.arg ↔ 0 ≤ z.im

Tactic:
calc
    0 ≤ arg z ↔ 0 ≤ Real.sin (arg z) :=
      ⟨fun h => Real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩, by
        contrapose!
        intro h
        exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)⟩
    _ ↔ _ := by rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]

Premises used: Complex.arg, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ z.arg < 0 ↔ z.im < 0

Tactic:
lt_iff_lt_of_le_iff_le arg_nonneg_iff

Premises used: Complex.arg_nonneg_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
r : ℝ
hr : 0 < r
inl : ((↑r : ℂ) * 0).arg = arg 0
inr : ∀ (hx : x ≠ 0), ((↑r : ℂ) * x).arg = x.arg
⊢ ((↑r : ℂ) * x).arg = x.arg

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
inl inl₁ : arg 0 = arg 0
⊢ ((↑r : ℂ) * 0).arg = arg 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
rw : x.arg
| ((↑r : ℂ) * x).arg

Tactic:
rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]

Premises used: Iff.mpr, norm_pos_iff, mul_assoc, Complex.arg_mul_cos_add_sin_mul_I, Complex.arg_mem_Ioc, Complex.norm_mul_cos_add_sin_mul_I, mul_pos, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
conv_lhs : ((↑r : ℂ) * x).arg = x.arg
inr : x.arg = x.arg
⊢ ((↑r : ℂ) * x).arg = x.arg

Tactic:
conv_lhs =>
    rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
      arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]

Premises used: Iff.mpr, norm_pos_iff, mul_assoc, Complex.arg_mul_cos_add_sin_mul_I, Complex.arg_mem_Ioc, Complex.norm_mul_cos_add_sin_mul_I, mul_pos, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
x : ℂ
⊢ (x * (↑r : ℂ)).arg = x.arg

Tactic:
mul_comm x r ▸ arg_real_mul x hr

Premises used: Eq.rec, Complex.ofReal, mul_comm, Complex.arg_real_mul, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
simp : x.arg = y.arg ↔ ((↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x).arg = y.arg
⊢ x.arg = y.arg ↔ (↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x = y

Tactic:
simp only [ext_norm_arg_iff, norm_mul, norm_div, norm_real, norm_norm,
    div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hx), true_and]

Premises used: Iff.mpr, div_mul_cancel₀, norm_mul, Complex.norm_real, norm_norm, norm_ne_zero_iff, norm_div, Complex.ext_norm_arg_iff, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
hr : 0 < ‖y‖ / ‖x‖
⊢ x.arg = y.arg ↔ ((↑‖y‖ : ℂ) / (↑‖x‖ : ℂ) * x).arg = y.arg

Tactic:
rw [← ofReal_div, arg_real_mul]

Premises used: Complex.ofReal_div, Complex.arg_real_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖

Tactic:
div_pos (norm_pos_iff.mpr hy) (norm_pos_iff.mpr hx)

Premises used: Iff.mpr, norm_pos_iff, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖

Tactic:
exact div_pos (norm_pos_iff.mpr hy) (norm_pos_iff.mpr hx)

Premises used: Iff.mpr, norm_pos_iff, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ arg 1 = 0

Tactic:
simp [arg, zero_le_one]

Premises used: Complex.arg, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
inl : (0 / 0).arg = 0
inr : ∀ (hx : x ≠ 0), (x / x).arg = 0
⊢ (x / x).arg = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ (0 / 0).arg = 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : x ≠ 0
⊢ (x / x).arg = 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ arg (-1) = π

Tactic:
simp [arg]

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ I.arg = π / 2

Tactic:
simp [arg]

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ (-I).arg = -(π / 2)

Tactic:
simp [arg]

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
pos : ∀ (h : x = 0), Real.tan x.arg = x.im / x.re
neg : ∀ (h : ¬x = 0), Real.tan x.arg = x.im / x.re
⊢ Real.tan x.arg = x.im / x.re

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : x = 0
⊢ Real.tan x.arg = x.im / x.re

Tactic:
simp only [h, zero_div, Complex.zero_im, Complex.arg_zero, Real.tan_zero, Complex.zero_re]

Premises used: zero_div, Complex.zero_im, Complex.arg_zero, Complex.zero_re, Real.tan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
h : ¬x = 0
neg : Real.sin x.arg / Real.cos x.arg = x.im / x.re
neg₁ : x.im / ‖x‖ / Real.cos x.arg = x.im / x.re
neg₂ : x.im / ‖x‖ / (x.re / ‖x‖) = x.im / x.re
neg₃ neg₄ : x.im / x.re = x.im / x.re
⊢ Real.tan x.arg = x.im / x.re

Tactic:
rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
    div_div_div_cancel_right₀ (norm_ne_zero_iff.mpr h)]

Premises used: Iff.mpr, div_div_div_cancel_right₀, norm_ne_zero_iff, Complex.sin_arg, Complex.cos_arg, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (↑x : ℂ).arg = 0

Tactic:
simp [arg, hx]

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
n : ℕ
⊢ arg (↑n : ℂ) = 0

Tactic:
ofReal_natCast n ▸ arg_ofReal_of_nonneg n.cast_nonneg

Premises used: Nat.cast_nonneg, Complex.arg_ofReal_of_nonneg, Eq.rec, Complex.ofReal_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ arg (OfNat.ofNat n) = 0

Tactic:
natCast_arg

Premises used: Complex.natCast_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
refine_1 : ∀ (h : z.arg = 0), 0 ≤ z.re ∧ z.im = 0
refine_2 : 0 ≤ z.re ∧ z.im = 0 → z.arg = 0
⊢ z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h : z.arg = 0
refine_1 :
  0 ≤ ((↑‖z‖ : ℂ) * (cos (↑0 : ℂ) + sin (↑0 : ℂ) * I)).re ∧ ((↑‖z‖ : ℂ) * (cos (↑0 : ℂ) + sin (↑0 : ℂ) * I)).im = 0
⊢ 0 ≤ z.re ∧ z.im = 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Premises used: Complex.norm_mul_cos_add_sin_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h : z.arg = 0
⊢ 0 ≤ ((↑‖z‖ : ℂ) * (cos (↑0 : ℂ) + sin (↑0 : ℂ) * I)).re ∧ ((↑‖z‖ : ℂ) * (cos (↑0 : ℂ) + sin (↑0 : ℂ) * I)).im = 0

Tactic:
simp [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
refine_2 :
  ∀ (x y : ℝ), 0 ≤ { re := x, im := y : ℂ }.re ∧ { re := x, im := y : ℂ }.im = 0 → { re := x, im := y : ℂ }.arg = 0
⊢ 0 ≤ z.re ∧ z.im = 0 → z.arg = 0

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℝ
h : 0 ≤ { re := x, im := 0 : ℂ }.re
⊢ { re := x, im := 0 : ℂ }.arg = 0

Tactic:
arg_ofReal_of_nonneg h

Premises used: Complex.arg_ofReal_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℝ
h : 0 ≤ { re := x, im := 0 : ℂ }.re
⊢ { re := x, im := 0 : ℂ }.arg = 0

Tactic:
exact arg_ofReal_of_nonneg h

Premises used: Complex.arg_ofReal_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : 0 ≤ z.re ∧ z.im = 0 ↔ 0 ≤ z
rw₁ : 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z
rw₂ rw₃ : 0 ≤ z.re ∧ 0 = z.im ↔ 0 ≤ z.re ∧ 0 = z.im
⊢ z.arg = 0 ↔ 0 ≤ z

Tactic:
rw [arg_eq_zero_iff, eq_comm, nonneg_iff]

Premises used: eq_comm, Complex.arg_eq_zero_iff, Complex.nonneg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
pos : ∀ (h₀ : z = 0), z.arg = π ↔ z.re < 0 ∧ z.im = 0
neg : ∀ (h₀ : ¬z = 0), z.arg = π ↔ z.re < 0 ∧ z.im = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
by_cases h₀ : z = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z = 0
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
simp [h₀, Real.pi_ne_zero.symm]

Premises used: Ne.symm, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
neg : z.arg = π → z.re < 0 ∧ z.im = 0
neg₁ : z.re < 0 ∧ z.im = 0 → z.arg = π
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
neg : ((↑‖z‖ : ℂ) * (cos (↑π : ℂ) + sin (↑π : ℂ) * I)).re < 0 ∧ ((↑‖z‖ : ℂ) * (cos (↑π : ℂ) + sin (↑π : ℂ) * I)).im = 0
⊢ z.re < 0 ∧ z.im = 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Premises used: Complex.norm_mul_cos_add_sin_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = π
⊢ ((↑‖z‖ : ℂ) * (cos (↑π : ℂ) + sin (↑π : ℂ) * I)).re < 0 ∧ ((↑‖z‖ : ℂ) * (cos (↑π : ℂ) + sin (↑π : ℂ) * I)).im = 0

Tactic:
simp [h₀]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
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 = π
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 : ℂ } = 0
neg : { re := x, im := 0 : ℂ }.arg = ((↑(-x) : ℂ) * -1).arg
⊢ { re := x, im := 0 : ℂ }.arg = π

Tactic:
rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]

Premises used: Iff.mpr, neg_pos, Complex.arg_neg_one, Complex.arg_real_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 : ℂ } = 0
⊢ { re := x, im := 0 : ℂ }.arg = ((↑(-x) : ℂ) * -1).arg

Tactic:
simp [← ofReal_def]

Premises used: Complex.ofReal_def
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ z.arg = π ↔ z < 0

Tactic:
arg_eq_pi_iff

Premises used: Complex.arg_eq_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
rw : z.arg ≠ π ↔ 0 ≤ z.re ∨ z.im ≠ 0
rw₁ : ¬(0 ≤ z.re ∨ z.im ≠ 0) ↔ z.arg = π
rw₂ : ¬0 ≤ z.re ∧ ¬z.im ≠ 0 ↔ z.arg = π
rw₃ : z.re < 0 ∧ ¬z.im ≠ 0 ↔ z.arg = π
rw₄ : z.re < 0 ∧ z.im = 0 ↔ z.arg = π
rw₅ rw₆ : z.re < 0 ∧ z.im = 0 ↔ z.re < 0 ∧ z.im = 0
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]

Premises used: not_le, Complex.arg_le_pi, Classical.not_not, not_or, LE.le.lt_iff_ne, Complex.arg_eq_pi_iff, not_iff_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℝ
hx : x < 0
⊢ (↑x : ℂ).arg = π

Tactic:
arg_eq_pi_iff.2 ⟨hx, rfl⟩

Premises used: Iff.mpr, And.intro, Complex.arg_eq_pi_iff, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
pos : ∀ (h₀ : z = 0), z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
neg : ∀ (h₀ : ¬z = 0), z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
by_cases h₀ : z = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
simp [h₀, Real.pi_div_two_pos.ne]

Premises used: Real.pi_div_two_pos, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
neg : z.arg = π / 2 → z.re = 0 ∧ 0 < z.im
neg₁ : z.re = 0 ∧ 0 < z.im → z.arg = π / 2
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
neg :
  ((↑‖z‖ : ℂ) * (cos (↑(π / 2) : ℂ) + sin (↑(π / 2) : ℂ) * I)).re = 0 ∧
    0 < ((↑‖z‖ : ℂ) * (cos (↑(π / 2) : ℂ) + sin (↑(π / 2) : ℂ) * I)).im
⊢ z.re = 0 ∧ 0 < z.im

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Premises used: Complex.norm_mul_cos_add_sin_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ ((↑‖z‖ : ℂ) * (cos (↑(π / 2) : ℂ) + sin (↑(π / 2) : ℂ) * I)).re = 0 ∧
    0 < ((↑‖z‖ : ℂ) * (cos (↑(π / 2) : ℂ) + sin (↑(π / 2) : ℂ) * I)).im

Tactic:
simp [h₀]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
neg :
  ∀ (x y : ℝ) (h₀ : ¬{ re := x, im := y : ℂ } = 0),
    { re := x, im := y : ℂ }.re = 0 ∧ 0 < { re := x, im := y : ℂ }.im → { re := x, im := y : ℂ }.arg = π / 2
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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
neg₆ neg₇ : { re := 0, im := y : ℂ }.arg = { re := 0, im := y }.arg
⊢ { re := 0, im := y : ℂ }.arg = π / 2

Tactic:
rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]

Premises used: Complex.ofReal_mul', Complex.I_re, Complex.I_im, MulZeroClass.mul_zero, Complex.arg_real_mul, mul_one, Complex.arg_I, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
pos : ∀ (h₀ : z = 0), z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
neg : ∀ (h₀ : ¬z = 0), z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
by_cases h₀ : z = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
simp [h₀, Real.pi_ne_zero]

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
neg : z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0
neg₁ : z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
neg :
  ((↑‖z‖ : ℂ) * (cos (↑(-(π / 2)) : ℂ) + sin (↑(-(π / 2)) : ℂ) * I)).re = 0 ∧
    ((↑‖z‖ : ℂ) * (cos (↑(-(π / 2)) : ℂ) + sin (↑(-(π / 2)) : ℂ) * I)).im < 0
⊢ z.re = 0 ∧ z.im < 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Premises used: Complex.norm_mul_cos_add_sin_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ ((↑‖z‖ : ℂ) * (cos (↑(-(π / 2)) : ℂ) + sin (↑(-(π / 2)) : ℂ) * I)).re = 0 ∧
    ((↑‖z‖ : ℂ) * (cos (↑(-(π / 2)) : ℂ) + sin (↑(-(π / 2)) : ℂ) * I)).im < 0

Tactic:
simp [h₀]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₀ : ¬z = 0
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)
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : y < 0
neg : ((↑0 : ℂ) + (↑y : ℂ) * I).arg = ((↑(-y) : ℂ) * -I).arg
⊢ { re := 0, im := y : ℂ }.arg = -(π / 2)

Tactic:
rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]

Premises used: Iff.mpr, Complex.mk_eq_add_mul_I, Complex.arg_neg_I, neg_pos, Complex.arg_real_mul, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
y : ℝ
h₀ : ¬{ re := 0, im := y : ℂ } = 0
hy : y < 0
⊢ ((↑0 : ℂ) + (↑y : ℂ) * I).arg = ((↑(-y) : ℂ) * -I).arg

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx : 0 ≤ x.re
⊢ x.arg = Real.arcsin (x.im / ‖x‖)

Tactic:
if_pos hx

Premises used: Complex.arg, if_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : 0 ≤ x.im
⊢ x.arg = Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
simp only [arg, hx_re.not_ge, hx_im, if_true, if_false]

Premises used: if_true, if_false, Complex.arg, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ x.arg = Real.arcsin ((-x).im / ‖x‖) - π

Tactic:
simp only [arg, hx_re.not_ge, hx_im.not_ge, if_false]

Premises used: if_false, Complex.arg, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
rw : z.arg = Real.arccos (Real.cos z.arg)
rw₁ rw₂ : z.arg = z.arg
⊢ z.arg = Real.arccos (z.re / ‖z‖)

Tactic:
rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]

Premises used: Iff.mpr, Complex.arg_le_pi, Real.arccos_cos, Complex.arg_nonneg_iff, Complex.cos_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : 0 < z.im
⊢ z.arg = Real.arccos (z.re / ‖z‖)

Tactic:
arg_of_im_nonneg_of_ne_zero hz.le fun h => hz.ne' <| h.symm ▸ rfl

Premises used: Eq.rec, LT.lt.le, Complex.arg_of_im_nonneg_of_ne_zero, LT.lt.ne', Eq.symm, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z.im < 0
⊢ z ≠ 0

Tactic:
have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
hx₁ : 0 ≤ -z.arg
hx₂ : -z.arg ≤ π
⊢ z.arg = -Real.arccos (z.re / ‖z‖)

Tactic:
rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg]

Premises used: neg_neg, Real.cos_neg, Real.arccos_cos, Complex.cos_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

Tactic:
neg_nonneg.2 (arg_neg_iff.2 hz).le

Premises used: Iff.mpr, LT.lt.le, neg_nonneg, Complex.arg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π

Tactic:
neg_le.2 (neg_pi_lt_arg z).le

Premises used: Iff.mpr, neg_le, LT.lt.le, Complex.neg_pi_lt_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

Tactic:
exacts [neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le]

Premises used: Iff.mpr, neg_le, LT.lt.le, Complex.neg_pi_lt_arg, neg_nonneg, Complex.arg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x : ℂ
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‖) - π
⊢ arg ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = if x.arg = π then π else -x.arg

Tactic:
simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, norm_conj, neg_div, neg_neg,
    Real.arcsin_neg]

Premises used: Complex.norm_conj, neg_div, neg_neg, Complex.arg, Complex.conj_im, Real.arcsin_neg, Complex.conj_re, Complex.arg_eq_pi_iff, Complex.neg_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
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‖) - π
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‖) - π
⊢ (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)

Premises used: Complex.re, OfNat.ofNat, lt_trichotomy