awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have rw₁ : (↑((↑n : ℝ) * θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
Tactic: rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₁ : (↑((↑n : ℝ) * θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have rw₂ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
Tactic: rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₁ : (↑((↑n : ℝ) * θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₂ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have rw₃ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π / (↑n : ℝ) < θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
Tactic: rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₁ : (↑((↑n : ℝ) * θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₂ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₃ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π / (↑n : ℝ) < θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have rw₄ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π < (↑n : ℝ) * θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
Tactic: rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₁ : (↑((↑n : ℝ) * θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₂ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₃ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π / (↑n : ℝ) < θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
rw₄ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π < (↑n : ℝ) * θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have rw₅ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π
Tactic: rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
have rw : (θ + θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
have rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
have rw₂ : θ.toReal ∈ Set.Ioc (-π / 2) (π / 2) ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
k : ℤ
⊢ (↑θ : Angle).toReal = θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ↔
    θ ∈ Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π)
have rw : -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π ↔
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
Tactic: rw [← sub_zero (θ : Angle), ← zsmul_zero k, ← coe_two_pi, ← coe_zsmul, ← coe_sub, zsmul_eq_mul, ←
    mul_assoc, mul_comm (k : ℝ), toReal_coe_eq_self_iff, Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
k : ℤ
h : -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ
have linarith : θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π →
  -π - (θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π) + (θ - (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
k : ℤ
h : -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π
⊢ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
have linarith : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π < θ →
  θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π - π + ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π - θ) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
k : ℤ
h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
⊢ -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π
have linarith : θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ -π →
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π - θ + (θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π - -π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
k : ℤ
h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
⊢ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π
have linarith : π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π →
  θ - (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π + (π - (θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)
have h : 2 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
Tactic: convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 2 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
⊢ (↑θ : Angle).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)
have h₁ : π = (HMul.hMul (α := ℝ) 2 (↑1 : ℝ) - 1) * π
Tactic: convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 2 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
h₁ : π = (HMul.hMul (α := ℝ) 2 (↑1 : ℝ) - 1) * π
⊢ (↑θ : Angle).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)
have h₂ : 3 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ) + 1
Tactic: convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)
have h : θ + 2 * π = θ - HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) * π
Tactic: convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : θ + 2 * π = θ - HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) * π
⊢ (↑θ : Angle).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)
have h₁ : Set.Ioc (-3 * π) (-π) =
  Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) + 1) * π)
Tactic: convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
have nth_rw : (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
Tactic: nth_rw 1 [← coe_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
have rw : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal
Tactic: rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
⊢ π / 2 < θ.toReal
have linarith : θ.toReal ≤ π / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
linarith : θ.toReal ≤ π / 2 → 2 / 2 = 1
⊢ π / 2 < θ.toReal
have linarith₁ : θ.toReal ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
linarith : θ.toReal ≤ π / 2 → 2 / 2 = 1
linarith₁ : θ.toReal ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 < θ.toReal
have linarith₂ : θ.toReal ≤ π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
linarith : θ.toReal ≤ π / 2 → 2 / 2 = 1
linarith₁ : θ.toReal ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ.toReal ≤ π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 < θ.toReal
have linarith₃ : θ.toReal ≤ π / 2 → π - 2 * θ.toReal + (2 * θ.toReal - 1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π / 2 < θ.toReal
⊢ 2 * θ.toReal ≤ 3 * π
have linarith : 3 * π < 2 * θ.toReal → 2 / 2 = 1
Tactic: linarith [pi_pos, toReal_le_pi θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π / 2 < θ.toReal
linarith : 3 * π < 2 * θ.toReal → 2 / 2 = 1
⊢ 2 * θ.toReal ≤ 3 * π
have linarith₁ : 3 * π < 2 * θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos, toReal_le_pi θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π / 2 < θ.toReal
linarith : 3 * π < 2 * θ.toReal → 2 / 2 = 1
linarith₁ : 3 * π < 2 * θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2 * θ.toReal ≤ 3 * π
have linarith₂ : 3 * π < 2 * θ.toReal → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos, toReal_le_pi θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : π / 2 < θ.toReal
linarith : 3 * π < 2 * θ.toReal → 2 / 2 = 1
linarith₁ : 3 * π < 2 * θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 3 * π < 2 * θ.toReal → GT.gt (α := ℝ) 2 0
⊢ 2 * θ.toReal ≤ 3 * π
have linarith₃ : 3 * π < 2 * θ.toReal → 3 * π - 2 * θ.toReal + (0 - π) + 2 * (θ.toReal - π) = 0
Tactic: linarith [pi_pos, toReal_le_pi θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
have rw : (θ + θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
have rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
have rw₂ : π / 2 < θ.toReal ↔ π / 2 < θ.toReal
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
have nth_rw : (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Tactic: nth_rw 1 [← coe_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
have rw : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2
Tactic: rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
⊢ θ.toReal ≤ -π / 2
have linarith : -π / 2 < θ.toReal → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
linarith : -π / 2 < θ.toReal → 2 / 2 = 1
⊢ θ.toReal ≤ -π / 2
have linarith₁ : -π / 2 < θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
linarith : -π / 2 < θ.toReal → 2 / 2 = 1
linarith₁ : -π / 2 < θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
⊢ θ.toReal ≤ -π / 2
have linarith₂ : -π / 2 < θ.toReal → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
linarith : -π / 2 < θ.toReal → 2 / 2 = 1
linarith₁ : -π / 2 < θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -π / 2 < θ.toReal → GT.gt (α := ℝ) 2 0
⊢ θ.toReal ≤ -π / 2
have linarith₃ : -π / 2 < θ.toReal → 2 * θ.toReal - -π + (-(1 * π) - 2 * θ.toReal) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.toReal ≤ -π / 2
⊢ -3 * π < 2 * θ.toReal
have linarith : 2 * θ.toReal ≤ -3 * π → 2 / 2 = 1
Tactic: linarith [pi_pos, neg_pi_lt_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.toReal ≤ -π / 2
linarith : 2 * θ.toReal ≤ -3 * π → 2 / 2 = 1
⊢ -3 * π < 2 * θ.toReal
have linarith₁ : 2 * θ.toReal ≤ -3 * π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos, neg_pi_lt_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.toReal ≤ -π / 2
linarith : 2 * θ.toReal ≤ -3 * π → 2 / 2 = 1
linarith₁ : 2 * θ.toReal ≤ -3 * π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -3 * π < 2 * θ.toReal
have linarith₂ : 2 * θ.toReal ≤ -3 * π → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos, neg_pi_lt_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.toReal ≤ -π / 2
linarith : 2 * θ.toReal ≤ -3 * π → 2 / 2 = 1
linarith₁ : 2 * θ.toReal ≤ -3 * π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * θ.toReal ≤ -3 * π → GT.gt (α := ℝ) 2 0
⊢ -3 * π < 2 * θ.toReal
have linarith₃ : 2 * θ.toReal ≤ -3 * π → 2 * θ.toReal - -3 * π + (0 - π) + 2 * (-π - θ.toReal) = 0
Tactic: linarith [pi_pos, neg_pi_lt_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
have rw : (θ + θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_add_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
have rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_add_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
have rw₂ : θ.toReal ≤ -π / 2 ↔ θ.toReal ≤ -π / 2
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_add_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
| θ.sin
have rw : Real.sin θ.toReal
Tactic: rw [← coe_toReal θ, sin_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ Real.sin θ.toReal = θ.sin
have conv_rhs : Real.sin θ.toReal = θ.sin
Tactic: conv_rhs => rw [← coe_toReal θ, sin_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
conv_rhs : Real.sin θ.toReal = θ.sin
⊢ Real.sin θ.toReal = θ.sin
have conv_rhs₁ : Real.sin θ.toReal = Real.sin θ.toReal
Tactic: conv_rhs => rw [← coe_toReal θ, sin_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
| θ.cos
have rw : Real.cos θ.toReal
Tactic: rw [← coe_toReal θ, cos_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ Real.cos θ.toReal = θ.cos
have conv_rhs : Real.cos θ.toReal = θ.cos
Tactic: conv_rhs => rw [← coe_toReal θ, cos_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
conv_rhs : Real.cos θ.toReal = θ.cos
⊢ Real.cos θ.toReal = θ.cos
have conv_rhs₁ : Real.cos θ.toReal = Real.cos θ.toReal
Tactic: conv_rhs => rw [← coe_toReal θ, cos_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
have this : 0 < π / 2
Tactic: have : 0 < π / 2 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
this : 0 < π / 2
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
have this₁ : θ.toReal ∈ Set.Ioc (-π) π
Tactic: have := toReal_mem_Ioc θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
this_1 : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
have rw : 0 ≤ Real.cos |θ.toReal| ↔ |θ.toReal| ≤ π / 2
Tactic: rw [← cos_toReal, ← cos_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ 0 < θ.cos ↔ |θ.toReal| < π / 2
have rw : |θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)
Tactic: rw [lt_iff_le_and_ne, lt_iff_le_and_ne, cos_nonneg_iff_abs_toReal_le_pi_div_two, ←
    and_congr_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ |θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos
have contrapose : |θ.toReal| = π / 2 ↔ 0 = θ.cos
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ |θ.toReal| = π / 2 ↔ 0 = θ.cos
have rw : |θ.toReal| = π / 2 ↔ θ.cos = 0
Tactic: rw [@eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : |θ.toReal| = π / 2 ↔ θ.cos = 0
⊢ |θ.toReal| = π / 2 ↔ 0 = θ.cos
have rw₁ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ.cos = 0
Tactic: rw [@eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : |θ.toReal| = π / 2 ↔ θ.cos = 0
rw₁ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ.cos = 0
⊢ |θ.toReal| = π / 2 ↔ 0 = θ.cos
have rw₂ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [@eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ ↔ θ = ψ
have suffices : θ ≠ ψ + (↑π : Angle)
Tactic: suffices θ ≠ ψ + π by simp [this, two_nsmul_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
ψ : Angle
hψ : |ψ.toReal| < π / 2
hθ : |(ψ + (↑π : Angle)).toReal| < π / 2
⊢ False
have hθ₁ : 0 < -ψ.cos
Tactic: simp only [← cos_pos_iff_abs_toReal_lt_pi_div_two, cos_add_pi] at hθ hψ
Cleared hypotheses: hψ, hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
ψ : Angle
hψ : |ψ.toReal| < π / 2
hθ : |(ψ + (↑π : Angle)).toReal| < π / 2
hθ₁ : 0 < -ψ.cos
⊢ False
have hψ₁ : 0 < ψ.cos
Tactic: simp only [← cos_pos_iff_abs_toReal_lt_pi_div_two, cos_add_pi] at hθ hψ
Cleared hypotheses: hψ, hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ HSMul.hSMul (α := ℤ) 2 θ = HSMul.hSMul (α := ℤ) 2 ψ ↔ θ = ψ
have simp_rw : θ + θ = ψ + ψ ↔ θ = ψ
Tactic: simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two hθ hψ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
simp_rw : θ + θ = ψ + ψ ↔ θ = ψ
⊢ HSMul.hSMul (α := ℤ) 2 θ = HSMul.hSMul (α := ℤ) 2 ψ ↔ θ = ψ
have simp_rw₁ : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ ↔ θ = ψ
Tactic: simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two hθ hψ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.cos < 0 ↔ π / 2 < |θ.toReal|
have contrapose! : 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ |θ.cos| = |ψ.sin|
have h₁ : θ = (↑(π / 2) : Angle) - ψ ∨ θ = (↑(π / 2) : Angle) - ψ + (↑π : Angle)
Tactic: rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h
Cleared hypotheses: h