awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
simp :
  (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
⊢ (if 0 ≤ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).re then
      Real.arcsin (((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).im / r)
    else
      if 0 ≤ ((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).im then
        Real.arcsin ((-((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I))).im / r) + π
      else Real.arcsin ((-((↑r : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I))).im / r) - π) =
    θ

Tactic:
simp only [re_ofReal_mul, im_ofReal_mul, neg_im, ← ofReal_cos, ← ofReal_sin, ←
    mk_eq_add_mul_I, neg_div, mul_div_cancel_left₀ _ hr.ne', mul_nonneg_iff_right_nonneg_of_pos hr]

Premises used: Complex.mk_eq_add_mul_I, neg_div, mul_div_cancel_left₀, LT.lt.ne', Complex.ofReal_cos, Complex.im_ofReal_mul, Complex.ofReal_sin, mul_nonneg_iff_right_nonneg_of_pos, Complex.neg_im, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
pos :
  ∀ (h₁ : θ ∈ Icc (-(π / 2)) (π / 2)),
    (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
      else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
      θ
neg :
  ∀ (h₁ : θ ∉ Icc (-(π / 2)) (π / 2)),
    (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
      else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
      θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
by_cases h₁ : θ ∈ Set.Icc (-(π / 2)) (π / 2)

Premises used: Real.pi, HDiv.hDiv, Set.Icc, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
pos : Real.arcsin (Real.sin θ) = θ
pos₁ : 0 ≤ Real.cos θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [if_pos]

Premises used: if_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ Real.arcsin (Real.sin θ) = θ

Tactic:
Real.arcsin_sin' h₁

Premises used: Real.arcsin_sin'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ Real.cos θ

Tactic:
Real.cos_nonneg_of_mem_Icc h₁

Premises used: Real.cos_nonneg_of_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ Real.arcsin (Real.sin θ) = θ

Tactic:
exacts [Real.arcsin_sin' h₁, Real.cos_nonneg_of_mem_Icc h₁]

Premises used: Real.cos_nonneg_of_mem_Icc, Real.arcsin_sin'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ ∉ Icc (-(π / 2)) (π / 2)
⊢ θ < -(π / 2) ∨ π / 2 < θ

Tactic:
rw [Set.mem_Icc, not_and_or, not_le, not_le] at h₁

Premises used: not_le, not_and_or, Set.mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
neg :
  ∀ (h₁ : θ < -(π / 2)),
    (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
      else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
      θ
neg₁ :
  ∀ (h₁ : π / 2 < θ),
    (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
      else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
      θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rcases h₁ with h₁ | h₁
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2)
⊢ -π < θ

Tactic:
replace hθ := hθ.1
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
rw : 0 < Real.cos (θ + π)
⊢ Real.cos θ < 0

Tactic:
rw [← neg_pos, ← Real.cos_add_pi]

Premises used: Real.cos_add_pi, neg_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)

Tactic:
Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩

Premises used: Real.cos_pos_of_mem_Ioo, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
refine_1 : -(π / 2) < θ + π
refine_2 : θ + π < π / 2
⊢ 0 < Real.cos (θ + π)

Tactic:
refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩

Premises used: Real.cos_pos_of_mem_Ioo, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : θ + π ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : θ + π ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : θ + π ≤ -(π / 2) → 2 * θ - -(1 * π) + 4 * (-π - θ) + (2 * θ + 2 * π - -(1 * π)) = 0
linarith₇ : θ + π ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) < θ + π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
linarith : π / 2 ≤ θ + π → 2 / 2 = 1
linarith₁ : π / 2 ≤ θ + π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ θ + π → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ θ + π → 2 / 2 = 1
linarith₄ : π / 2 ≤ θ + π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 ≤ θ + π → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 ≤ θ + π → 2 * θ - -(1 * π) + (1 * π - (2 * θ + 2 * π)) = 0
⊢ θ + π < π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ Real.cos θ < 0

Tactic:
have hcos : Real.cos θ < 0 := by
        rw [← neg_pos, ← Real.cos_add_pi]
        refine Real.cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
linarith : 0 ≤ θ → 2 / 2 = 1
linarith₁ : 0 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 ≤ θ → GT.gt (α := ℝ) 2 0
linarith₃ : 0 ≤ θ → 2 * θ - -(1 * π) + (-π - θ) + (0 - θ) = 0
⊢ θ < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
⊢ Real.sin θ < 0

Tactic:
have hsin : Real.sin θ < 0 := Real.sin_neg_of_neg_of_neg_pi_lt (by linarith) hθ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
neg : -(π / 2) ≤ θ + π
neg₁ : θ + π ≤ π / 2
neg₂ : ¬0 ≤ Real.sin θ
neg₃ : ¬0 ≤ Real.cos θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right]

Premises used: Real.arcsin_sin, add_sub_cancel_right, Real.sin_add_pi, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
linarith : θ + π < -(π / 2) → 2 / 2 = 1
linarith₁ : θ + π < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ + π < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : θ + π < -(π / 2) → 2 / 2 = 1
linarith₄ : θ + π < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : θ + π < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : θ + π < -(π / 2) → 2 * θ - -(1 * π) + 4 * (-π - θ) + (2 * θ + 2 * π - -(1 * π)) = 0
linarith₇ : θ + π < -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) ≤ θ + π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
linarith : π / 2 < θ + π → 2 / 2 = 1
linarith₁ : π / 2 < θ + π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < θ + π → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 < θ + π → 2 / 2 = 1
linarith₄ : π / 2 < θ + π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 < θ + π → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 < θ + π → 2 * θ - -(1 * π) + (1 * π - (2 * θ + 2 * π)) = 0
⊢ θ + π ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

Tactic:
hsin.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.sin θ

Tactic:
exact hsin.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ

Tactic:
hcos.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ ¬0 ≤ Real.cos θ

Tactic:
exact hcos.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
neg : (if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) = θ
neg₁ : ¬0 ≤ Real.cos θ
neg₂ : Real.arcsin (-Real.sin θ) - π = θ
neg₃ : ¬0 ≤ Real.sin θ
neg₄ : ¬0 ≤ Real.cos θ
neg₅ : Real.arcsin (Real.sin (θ + π)) - π = θ
neg₆ : ¬0 ≤ Real.sin θ
neg₇ : ¬0 ≤ Real.cos θ
neg₈ : θ + π - π = θ
neg₉ : -(π / 2) ≤ θ + π
neg₁₀ : θ + π ≤ π / 2
neg₁₁ : ¬0 ≤ Real.sin θ
neg₁₂ : ¬0 ≤ Real.cos θ
neg₁₃ : θ = θ
neg₁₄ : -(π / 2) ≤ θ + π
neg₁₅ : θ + π ≤ π / 2
neg₁₆ : ¬0 ≤ Real.sin θ
neg₁₇ : ¬0 ≤ Real.cos θ
neg₁₈ : θ = θ
neg₁₉ : -(π / 2) ≤ θ + π
neg₂₀ : θ + π ≤ π / 2
neg₂₁ : ¬0 ≤ Real.sin θ
neg₂₂ : ¬0 ≤ Real.cos θ
neg₂₃ : -(π / 2) ≤ θ + π
neg₂₄ : θ + π ≤ π / 2
neg₂₅ : ¬0 ≤ Real.sin θ
neg₂₆ : ¬0 ≤ Real.cos θ
neg₂₇ : -(π / 2) ≤ θ + π
neg₂₈ : θ + π ≤ π / 2
neg₂₉ : ¬0 ≤ Real.sin θ
neg₃₀ : ¬0 ≤ Real.cos θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [if_neg, if_neg, ← Real.sin_add_pi, Real.arcsin_sin, add_sub_cancel_right] <;> [linarith;
        linarith; exact hsin.not_ge; exact hcos.not_ge]

Premises used: Real.arcsin_sin, add_sub_cancel_right, LT.lt.not_ge, Real.sin_add_pi, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 2 < θ
⊢ θ ≤ π

Tactic:
replace hθ := hθ.2
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
linarith : π + π / 2 ≤ θ → 2 / 2 = 1
linarith₁ : π + π / 2 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π + π / 2 ≤ θ → GT.gt (α := ℝ) 2 0
linarith₃ : π + π / 2 ≤ θ → 2 / 2 = 1
linarith₄ : π + π / 2 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π + π / 2 ≤ θ → GT.gt (α := ℝ) 2 0
linarith₆ : π + π / 2 ≤ θ → 1 * π - 2 * θ + 4 * (θ - π) + (2 * π + 1 * π - 2 * θ) = 0
linarith₇ : π + π / 2 ≤ θ → GT.gt (α := ℝ) 4 0
⊢ θ < π + π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ Real.cos θ < 0

Tactic:
have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
linarith : θ < 0 → 2 / 2 = 1
linarith₁ : θ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : θ < 0 → 1 * π - 2 * θ + (θ - π) + (θ - 0) = 0
⊢ 0 ≤ θ

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ 0 ≤ Real.sin θ

Tactic:
have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
neg : -(π / 2) ≤ θ - π
neg₁ : θ - π ≤ π / 2
neg₂ : 0 ≤ Real.sin θ
neg₃ : ¬0 ≤ Real.cos θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel]

Premises used: if_pos, Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
linarith : θ - π < -(π / 2) → 2 / 2 = 1
linarith₁ : θ - π < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ - π < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : θ - π < -(π / 2) → 2 / 2 = 1
linarith₄ : θ - π < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : θ - π < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : θ - π < -(π / 2) → 1 * π - 2 * θ + (2 * θ - 2 * π - -(1 * π)) = 0
⊢ -(π / 2) ≤ θ - π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
linarith : π / 2 < θ - π → 2 / 2 = 1
linarith₁ : π / 2 < θ - π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < θ - π → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 < θ - π → 2 / 2 = 1
linarith₄ : π / 2 < θ - π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 < θ - π → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 < θ - π → 1 * π - 2 * θ + 4 * (θ - π) + (1 * π - (2 * θ - 2 * π)) = 0
linarith₇ : π / 2 < θ - π → GT.gt (α := ℝ) 4 0
⊢ θ - π ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ 0 ≤ Real.sin θ

Tactic:
hsin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ 0 ≤ Real.sin θ

Tactic:
exact hsin
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ

Tactic:
hcos.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ ¬0 ≤ Real.cos θ

Tactic:
exact hcos.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
neg : (if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) = θ
neg₁ : ¬0 ≤ Real.cos θ
neg₂ : Real.arcsin (-Real.sin θ) + π = θ
neg₃ : 0 ≤ Real.sin θ
neg₄ : ¬0 ≤ Real.cos θ
neg₅ : Real.arcsin (Real.sin (θ - π)) + π = θ
neg₆ : 0 ≤ Real.sin θ
neg₇ : ¬0 ≤ Real.cos θ
neg₈ : θ - π + π = θ
neg₉ : -(π / 2) ≤ θ - π
neg₁₀ : θ - π ≤ π / 2
neg₁₁ : 0 ≤ Real.sin θ
neg₁₂ : ¬0 ≤ Real.cos θ
neg₁₃ : θ = θ
neg₁₄ : -(π / 2) ≤ θ - π
neg₁₅ : θ - π ≤ π / 2
neg₁₆ : 0 ≤ Real.sin θ
neg₁₇ : ¬0 ≤ Real.cos θ
neg₁₈ : θ = θ
neg₁₉ : -(π / 2) ≤ θ - π
neg₂₀ : θ - π ≤ π / 2
neg₂₁ : 0 ≤ Real.sin θ
neg₂₂ : ¬0 ≤ Real.cos θ
neg₂₃ : -(π / 2) ≤ θ - π
neg₂₄ : θ - π ≤ π / 2
neg₂₅ : 0 ≤ Real.sin θ
neg₂₆ : ¬0 ≤ Real.cos θ
neg₂₇ : -(π / 2) ≤ θ - π
neg₂₈ : θ - π ≤ π / 2
neg₂₉ : 0 ≤ Real.sin θ
neg₃₀ : ¬0 ≤ Real.cos θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]

Premises used: if_pos, Real.sin_sub_pi, Real.arcsin_sin, LT.lt.not_ge, sub_add_cancel, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
hθ : θ ∈ Ioc (-π) π
rw : (1 * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
rw₁ : ((↑1 : ℂ) * (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I)).arg = θ
rw₂ rw₃ : θ = θ
⊢ (cos (↑θ : ℂ) + sin (↑θ : ℂ) * I).arg = θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]

Premises used: Complex.arg_mul_cos_add_sin_mul_I, Complex.ofReal_one, zero_lt_one, HAdd.hAdd, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ ((↑(rexp z.re) : ℂ) *
        (cos (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) + sin (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) * I)).arg =
    toIocMod Real.two_pi_pos (-π) z.im

Tactic:
arg_mul_cos_add_sin_mul_I (Real.exp_pos z.re) (θ := toIocMod Real.two_pi_pos (-π) z.im) _

Premises used: Complex.arg_mul_cos_add_sin_mul_I, Complex.re, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h :
  (cexp z).arg =
    ((↑(rexp z.re) : ℂ) *
        (cos (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) + sin (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) * I)).arg
arg_mul_cos_add_sin_mul_I : toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π
⊢ (cexp z).arg = toIocMod Real.two_pi_pos (-π) z.im

Tactic:
convert!
    arg_mul_cos_add_sin_mul_I (Real.exp_pos z.re) (θ := toIocMod Real.two_pi_pos (-π) z.im) _
    using 1

Premises used: Complex.arg_mul_cos_add_sin_mul_I, Complex.re, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) : ℂ) * I)).arg
⊢ (cexp z).arg =
    ((↑(rexp z.re) : ℂ) *
        (cos (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) + sin (↑(toIocMod Real.two_pi_pos (-π) z.im) : ℂ) * I)).arg

Tactic:
rw [← exp_mul_I, ofReal_exp, toIocMod]

Premises used: Complex.ofReal_exp, toIocMod, Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h :
  (cexp z).arg = (cexp (↑z.re : ℂ) * cexp (((↑z.im : ℂ) - toIocDiv Real.two_pi_pos (-π) z.im • (2 * (↑π : ℂ))) * I)).arg
⊢ (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) : ℂ) * I)).arg

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h : (cexp z).arg = (cexp (↑z.re : ℂ) * cexp ((↑z.im : ℂ) * I)).arg
h₁ : (cexp z).arg = (cexp ((↑z.re : ℂ) + (↑z.im : ℂ) * I)).arg
h₂ h₃ : (cexp z).arg = (cexp z).arg
⊢ (cexp z).arg = (cexp (↑z.re : ℂ) * cexp (((↑z.im : ℂ) - toIocDiv Real.two_pi_pos (-π) z.im • (2 * (↑π : ℂ))) * I)).arg

Tactic:
rw [exp_mul_I_periodic.sub_zsmul_eq, ← exp_add, re_add_im]

Premises used: Complex.exp_add, Function.Periodic.sub_zsmul_eq, Complex.re_add_im, Complex.exp_mul_I_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) (-π + 2 * π)

Tactic:
toIocMod_mem_Ioc ..

Premises used: toIocMod_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
h : π = -π + 2 * π
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π

Tactic:
convert! toIocMod_mem_Ioc ..

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

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
θ : ℝ
⊢ (cexp ((↑θ : ℂ) * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
simp [arg_exp]

Premises used: Complex.arg_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
⊢ arg 0 = 0

Tactic:
simp [arg]

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
rw : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = y
rw₁ : (↑‖x‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
rw₂ : (↑‖y‖ : ℂ) * cexp ((↑x.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
rw₃ rw₄ : (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I) = (↑‖y‖ : ℂ) * cexp ((↑y.arg : ℂ) * I)
⊢ x = y

Tactic:
rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]

Premises used: Complex.norm_mul_exp_arg_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
x y : ℂ
⊢ x = y ↔ ‖x‖ = ‖y‖ ∧ x.arg = y.arg

Tactic:
⟨fun h => h ▸ ⟨rfl, rfl⟩, and_imp.2 ext_norm_arg⟩

Premises used: Iff.mpr, and_imp, Eq.rec, Complex.ext_norm_arg, And.intro, Iff.intro, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ 0 < π

Tactic:
have hπ : 0 < π := Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
inl : arg 0 ∈ Ioc (-π) π
inr : ∀ (hz : z ≠ 0), z.arg ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π

Tactic:
simp [hπ, hπ.le]

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
inr : ∀ (N : ℤ) (hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)), z.arg ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩

Premises used: Real.pi, existsUnique_add_zsmul_mem_Ioc, Complex.arg, Real.two_pi_pos, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π

Tactic:
rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN

Premises used: zsmul_eq_mul, two_mul, neg_add_cancel_left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
inr :
  ((↑‖z‖ : ℂ) *
        (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg ∈
    Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]

Premises used: Complex.norm_mul_cos_add_sin_mul_I, Complex.sin_add_int_mul_two_pi, Complex.cos_add_int_mul_two_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
⊢ ((↑‖z‖ : ℂ) * (cos (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) + sin (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) * I)).arg =
    z.arg + (↑N : ℝ) * (2 * π)

Tactic:
have := arg_mul_cos_add_sin_mul_I (norm_pos_iff.mpr hz) hN
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
this :
  ((↑‖z‖ : ℂ) * (cos (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) + sin (↑(z.arg + (↑N : ℝ) * (2 * π)) : ℂ) * I)).arg =
    z.arg + (↑N : ℝ) * (2 * π)
⊢ ((↑‖z‖ : ℂ) *
        (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg =
    z.arg + (↑N : ℝ) * (2 * π)

Tactic:
push_cast at this
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
this :
  ((↑‖z‖ : ℂ) *
        (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg =
    z.arg + (↑N : ℝ) * (2 * π)
inr inr₁ inr₂ inr₃ : z.arg + (↑N : ℝ) * (2 * π) ∈ Ioc (-π) π
⊢ ((↑‖z‖ : ℂ) *
        (cos ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) + sin ((↑z.arg : ℂ) + (↑N : ℂ) * (2 * (↑π : ℂ))) * I)).arg ∈
    Ioc (-π) π

Tactic:
rwa [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg
Goal:
z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.arg = z.arg

Tactic:
simpa [toIocMod_eq_self, two_mul] using z.arg_mem_Ioc

Premises used: toIocMod_eq_self, two_mul, Complex.arg_mem_Ioc