awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ -(π / 2) ≤ θ + π
have linarith₂ : θ + π < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ -(π / 2) ≤ θ + π
have linarith₆ : θ + π < -(π / 2) → 2 * θ - -(1 * π) + 4 * (-π - θ) + (2 * θ + 2 * π - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ -(π / 2) ≤ θ + π
have linarith₇ : θ + π < -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ θ + π ≤ π / 2
have linarith : π / 2 < θ + π → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
linarith : π / 2 < θ + π → 2 / 2 = 1
⊢ θ + π ≤ π / 2
have linarith₁ : π / 2 < θ + π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ + π ≤ π / 2
have linarith₂ : π / 2 < θ + π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ + π ≤ π / 2
have linarith₆ : π / 2 < θ + π → 2 * θ - -(1 * π) + (1 * π - (2 * θ + 2 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
hcos : Real.cos θ < 0
hsin : Real.sin θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg : (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ) - π) = θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁ : ¬0 ≤ Real.cos θ
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₂ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ) - π = θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₃ : ¬0 ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₅ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₈ : θ + π - π = θ
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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₈ : θ + π - π = θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₉ : -(π / 2) ≤ θ + π
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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) ≤ θ + π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁₀ : θ + π ≤ π / 2
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁₃ : θ = θ
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
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 θ) - π) =
    θ
have hθ₁ : θ ≤ π
Tactic: replace hθ := hθ.2
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ θ < π + π / 2
have linarith : π + π / 2 ≤ θ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
linarith : π + π / 2 ≤ θ → 2 / 2 = 1
⊢ θ < π + π / 2
have linarith₁ : π + π / 2 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
linarith : π + π / 2 ≤ θ → 2 / 2 = 1
linarith₁ : π + π / 2 ≤ θ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ θ < π + π / 2
have linarith₂ : π + π / 2 ≤ θ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ < π + π / 2
have linarith₆ : π + π / 2 ≤ θ → 1 * π - 2 * θ + 4 * (θ - π) + (2 * π + 1 * π - 2 * θ) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ < π + π / 2
have linarith₇ : π + π / 2 ≤ θ → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have hcos : Real.cos θ < 0
Tactic: have hcos : Real.cos θ < 0 := Real.cos_neg_of_pi_div_two_lt_of_lt h₁ (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ 0 ≤ θ
have linarith : θ < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
linarith : θ < 0 → 2 / 2 = 1
⊢ 0 ≤ θ
have linarith₁ : θ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
linarith : θ < 0 → 2 / 2 = 1
linarith₁ : θ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ θ
have linarith₂ : θ < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ 0 ≤ θ
have linarith₃ : θ < 0 → 1 * π - 2 * θ + (θ - π) + (θ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (hypothesis)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have hsin : 0 ≤ Real.sin θ
Tactic: have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ 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 θ) - π) =
    θ
have neg : -(π / 2) ≤ θ - π
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
neg : -(π / 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 θ) - π) =
    θ
have neg₁ : θ - π ≤ π / 2
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
neg : -(π / 2) ≤ θ - π
neg₁ : θ - π ≤ π / 2
neg₂ : 0 ≤ 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 θ) - π) =
    θ
have neg₃ : ¬0 ≤ Real.cos θ
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ -(π / 2) ≤ θ - π
have linarith : θ - π < -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
linarith : θ - π < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ θ - π
have linarith₁ : θ - π < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ -(π / 2) ≤ θ - π
have linarith₂ : θ - π < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ -(π / 2) ≤ θ - π
have linarith₆ : θ - π < -(π / 2) → 1 * π - 2 * θ + (2 * θ - 2 * π - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ θ - π ≤ π / 2
have linarith : π / 2 < θ - π → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
linarith : π / 2 < θ - π → 2 / 2 = 1
⊢ θ - π ≤ π / 2
have linarith₁ : π / 2 < θ - π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ - π ≤ π / 2
have linarith₂ : π / 2 < θ - π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ - π ≤ π / 2
have linarith₆ : π / 2 < θ - π → 1 * π - 2 * θ + 4 * (θ - π) + (1 * π - (2 * θ - 2 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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
⊢ θ - π ≤ π / 2
have linarith₇ : π / 2 < θ - π → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
Goal:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ 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 θ) - π) =
    θ
have neg : (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ) - π) = θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁ : ¬0 ≤ Real.cos θ
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₂ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₅ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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 θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₈ : θ - π + π = θ
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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₈ : θ - π + π = θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₉ : -(π / 2) ≤ θ - π
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arg (goal)
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) ≤ θ - π
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
have neg₁₀ : θ - π ≤ π / 2
Tactic: rw [if_neg, if_pos, ← Real.sin_sub_pi, Real.arcsin_sin, sub_add_cancel] <;> [linarith;
        linarith; exact hsin; exact hcos.not_ge]