awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2
have linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ cos (π / 3) = 1 / 2
have linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ cos (π / 3) = 1 / 2
have linarith₃ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₈ : cos (π / 3) < 1 / 2 →
  HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
        2 * (1 * cos π - 1 * cos (π / 3)) +
      2 * -(cos π - -1) =
    0
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ cos (π / 3) = 1 / 2
have linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₁₂ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
linarith₁₂ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ cos (π / 3) = 1 / 2
have linarith₁₃ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 2 0
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
linarith₁₂ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 2 0
⊢ cos (π / 3) = 1 / 2
have linarith₁₄ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
linarith₁₂ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 2 0
linarith₁₄ linarith₁₅ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₁₆ : 1 / 2 < cos (π / 3) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
linarith₁₂ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 2 0
linarith₁₄ linarith₁₅ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₆ : 1 / 2 < cos (π / 3) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₇ linarith₁₈ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₁₉ : 1 / 2 < cos (π / 3) →
  HMul.hMul (α := ℝ) 3 (-1) +
        (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0) +
      (HMul.hMul (α := ℝ) 1 1 - 2 * cos (π / 3)) =
    0
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
linarith : cos (π / 3) < 1 / 2 → 2 / 2 = 1
linarith₁ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ linarith₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₈ :
  cos (π / 3) < 1 / 2 →
    HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0 +
          2 * (1 * cos π - 1 * cos (π / 3)) +
        2 * -(cos π - -1) =
      0
linarith₉ linarith₁₀ : cos (π / 3) < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
linarith₁₂ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 2 0
linarith₁₄ linarith₁₅ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₆ : 1 / 2 < cos (π / 3) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₇ linarith₁₈ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₉ :
  1 / 2 < cos (π / 3) →
    HMul.hMul (α := ℝ) 3 (-1) +
          (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2 - HMul.hMul (α := ℝ) 1 0) +
        (HMul.hMul (α := ℝ) 1 1 - 2 * cos (π / 3)) =
      0
⊢ cos (π / 3) = 1 / 2
have linarith₂₀ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 3 0
Tactic: linarith [cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 6) = √3 / 2
have rw : LE.le (α := ℝ) 0 2
Tactic: rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : LE.le (α := ℝ) 0 2
⊢ cos (π / 6) = √3 / 2
have hx : LE.le (α := ℝ) 0 3
Tactic: rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : LE.le (α := ℝ) 0 2
hx : LE.le (α := ℝ) 0 3
⊢ cos (π / 6) = √3 / 2
have rw₁ : Ne (α := ℝ) 2 0
Tactic: rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : LE.le (α := ℝ) 0 2
hx : LE.le (α := ℝ) 0 3
rw₁ : Ne (α := ℝ) 2 0
⊢ cos (π / 6) = √3 / 2
have hl : -π ≤ π / 3
Tactic: rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : LE.le (α := ℝ) 0 2
hx : LE.le (α := ℝ) 0 3
rw₁ : Ne (α := ℝ) 2 0
hl : -π ≤ π / 3
⊢ cos (π / 6) = √3 / 2
have hr : π / 3 ≤ π
Tactic: rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ LE.le (α := ℝ) 0 2
have linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
⊢ LE.le (α := ℝ) 0 2
have linarith₁ : LT.lt (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ LE.le (α := ℝ) 0 3
have linarith : LT.lt (α := ℝ) 3 0 → HMul.hMul (α := ℝ) 3 (-1) + HSub.hSub (α := ℝ) 3 0 = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : LT.lt (α := ℝ) 3 0 → HMul.hMul (α := ℝ) 3 (-1) + HSub.hSub (α := ℝ) 3 0 = 0
⊢ LE.le (α := ℝ) 0 3
have linarith₁ : LT.lt (α := ℝ) 3 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Ne (α := ℝ) 2 0
have linarith : Eq (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : Eq (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
⊢ Ne (α := ℝ) 2 0
have linarith₁ : Eq (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ -π ≤ π / 3
have linarith : π / 3 < -π → 3 / 3 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π / 3 < -π → 3 / 3 = 1
⊢ -π ≤ π / 3
have linarith₁ : π / 3 < -π → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π / 3 < -π → 3 / 3 = 1
linarith₁ : π / 3 < -π → HMul.hMul (α := ℝ) 1 3 = 3
⊢ -π ≤ π / 3
have linarith₂ : π / 3 < -π → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π / 3 < -π → 3 / 3 = 1
linarith₁ : π / 3 < -π → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < -π → GT.gt (α := ℝ) 3 0
⊢ -π ≤ π / 3
have linarith₃ : π / 3 < -π → 1 * π - -(3 * π) + 4 * (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π / 3 < -π → 3 / 3 = 1
linarith₁ : π / 3 < -π → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < -π → GT.gt (α := ℝ) 3 0
linarith₃ : π / 3 < -π → 1 * π - -(3 * π) + 4 * (0 - π) = 0
⊢ -π ≤ π / 3
have linarith₄ : π / 3 < -π → GT.gt (α := ℝ) 4 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ π / 3 ≤ π
have linarith : π < π / 3 → 3 / 3 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π < π / 3 → 3 / 3 = 1
⊢ π / 3 ≤ π
have linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ π / 3 ≤ π
have linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
⊢ π / 3 ≤ π
have linarith₃ : π < π / 3 → 3 * π - 1 * π + 2 * (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : π < π / 3 → 3 / 3 = 1
linarith₁ : π < π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π < π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : π < π / 3 → 3 * π - 1 * π + 2 * (0 - π) = 0
⊢ π / 3 ≤ π
have linarith₄ : π < π / 3 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (cos (π / 6)) 2 = 3 / 4
have rw : 3 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 3 / 4
Tactic: rw [cos_pi_div_six, div_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : 3 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 3 / 4
⊢ HPow.hPow (β := ℕ) (cos (π / 6)) 2 = 3 / 4
have rw₁ : LE.le (α := ℝ) 0 3
Tactic: rw [cos_pi_div_six, div_pow, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 6) = 1 / 2
have rw : cos (π / 2 - π / 6) = cos (π / 3)
Tactic: rw [← cos_pi_div_two_sub, ← cos_pi_div_three]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 2 - π / 6) = cos (π / 3)
have e_x : π / 2 - π / 6 = π / 3
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (sin (π / 3)) 2 = 3 / 4
have rw : HPow.hPow (β := ℕ) (cos (π / 2 - π / 3)) 2 = HPow.hPow (β := ℕ) (cos (π / 6)) 2
Tactic: rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (cos (π / 2 - π / 3)) 2 = HPow.hPow (β := ℕ) (cos (π / 6)) 2
have e_a : π / 2 - π / 3 = π / 6
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 3) = √3 / 2
have rw : cos (π / 2 - π / 3) = cos (π / 6)
Tactic: rw [← cos_pi_div_two_sub, ← cos_pi_div_six]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 2 - π / 3) = cos (π / 6)
have e_x : π / 2 - π / 3 = π / 6
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ 4 * HPow.hPow (β := ℕ) (cos (π / 5)) 2 - 2 * cos (π / 5) - 1 = 0
have set : let θ := π / 5;
∀ (hθ : θ = π / 5), 4 * HPow.hPow (β := ℕ) (cos θ) 2 - 2 * cos θ - 1 = 0
Tactic: set θ := π / 5 with hθ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0
have suffices : 2 * c = 4 * HPow.hPow (β := ℕ) c 2 - 1
Tactic: suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ s ≠ 0
have rw : ¬∃ (n : ℤ), (↑n : ℝ) * π = π / 5
Tactic: rw [ne_eq, sin_eq_zero_iff, hθ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ (n : ℤ), (↑n : ℝ) * π = π / 5
have push : ∀ (n : ℤ), (↑n : ℝ) * π ≠ π / 5
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : (↑n : ℝ) * π = π / 5
⊢ n * 5 = 1
have hn₁ : HMul.hMul (α := ℝ) (↑n : ℝ) 5 = 1
Tactic: field_simp at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : HMul.hMul (α := ℝ) (↑n : ℝ) 5 = 1
⊢ n * 5 = 1
have norm_cast : ∀ (hn : n * 5 = 1), n * 5 = 1
Tactic: norm_cast at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : (↑n : ℝ) * π = π / 5
⊢ False
have hn₁ : n * 5 = 1
Tactic: replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ 2 * c = 4 * HPow.hPow (β := ℕ) c 2 - 1
have hs : s ≠ 0
Tactic: have hs : s ≠ 0 := by
    rw [ne_eq, sin_eq_zero_iff, hθ]
    push Not
    intro n hn
    replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
    lia
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * c = 4 * HPow.hPow (β := ℕ) c 2 - 1
have suffices : s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
Tactic: suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ s * (2 * c) = 2 * s * c
have rw : s * 2 * c = 2 * s * c
Tactic: rw [← mul_assoc, mul_comm 2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
rw : s * 2 * c = 2 * s * c
⊢ s * (2 * c) = 2 * s * c
have rw₁ : s * 2 * c = s * 2 * c
Tactic: rw [← mul_assoc, mul_comm 2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c = sin (2 * θ)
have rw : 2 * s * c = 2 * sin θ * cos θ
Tactic: rw [sin_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ) = sin (π - 2 * θ)
have rw : sin (2 * θ) = sin (2 * θ)
Tactic: rw [sin_pi_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (π - 2 * θ) = sin (2 * θ + θ)
have e_x : π - 2 * θ = 2 * θ + θ
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ π - 2 * θ = 2 * θ + θ
have linarith : π - 2 * θ < 2 * θ + θ → 5 / 5 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
linarith : π - 2 * θ < 2 * θ + θ → 5 / 5 = 1
⊢ π - 2 * θ = 2 * θ + θ
have linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
Tactic: linarith