awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
this : cos (3 * (π / 3)) = cos π
linarith :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
linarith₁ linarith₂ linarith₃ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₅ linarith₆ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 →
    2 * -(1 * cos (3 * (π / 3)) - 1 * cos π) +
            (1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1) 2 *
                (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2) -
              HMul.hMul (α := ℝ) 1 0) +
          2 * -(cos π - -1) +
        2 *
          (1 * cos (3 * (π / 3)) -
            (HMul.hMul (α := ℝ) 1 4 * (1 * HPow.hPow (β := ℕ) (1 * cos (π / 3)) 3) -
              HMul.hMul (α := ℝ) 1 3 * (1 * cos (π / 3)))) =
      0
linarith₈ linarith₉ linarith₁₀ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → GT.gt (α := ℝ) 2 0
linarith₁₁ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
linarith₁₂ linarith₁₃ linarith₁₄ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₅ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₆ linarith₁₇ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have linarith₁₈ : 0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) →
  2 * (1 * cos (3 * (π / 3)) - 1 * cos π) +
          (HMul.hMul (α := ℝ) 1 0 -
            1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1) 2 *
              (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2)) +
        2 * (cos π - -1) +
      2 *
        -(1 * cos (3 * (π / 3)) -
            (HMul.hMul (α := ℝ) 1 4 * (1 * HPow.hPow (β := ℕ) (1 * cos (π / 3)) 3) -
              HMul.hMul (α := ℝ) 1 3 * (1 * cos (π / 3)))) =
    0
Tactic: linarith [cos_pi, cos_three_mul (π / 3)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
this : cos (3 * (π / 3)) = cos π
linarith :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
linarith₁ linarith₂ linarith₃ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₅ linarith₆ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 →
    2 * -(1 * cos (3 * (π / 3)) - 1 * cos π) +
            (1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1) 2 *
                (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2) -
              HMul.hMul (α := ℝ) 1 0) +
          2 * -(cos π - -1) +
        2 *
          (1 * cos (3 * (π / 3)) -
            (HMul.hMul (α := ℝ) 1 4 * (1 * HPow.hPow (β := ℕ) (1 * cos (π / 3)) 3) -
              HMul.hMul (α := ℝ) 1 3 * (1 * cos (π / 3)))) =
      0
linarith₈ linarith₉ linarith₁₀ :
  HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → GT.gt (α := ℝ) 2 0
linarith₁₁ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
linarith₁₂ linarith₁₃ linarith₁₄ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₅ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₆ linarith₁₇ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₈ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) →
    2 * (1 * cos (3 * (π / 3)) - 1 * cos π) +
            (HMul.hMul (α := ℝ) 1 0 -
              1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1) 2 *
                (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) + HMul.hMul (α := ℝ) 1 2)) +
          2 * (cos π - -1) +
        2 *
          -(1 * cos (3 * (π / 3)) -
              (HMul.hMul (α := ℝ) 1 4 * (1 * HPow.hPow (β := ℕ) (1 * cos (π / 3)) 3) -
                HMul.hMul (α := ℝ) 1 3 * (1 * cos (π / 3)))) =
      0
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have linarith₁₉ : 0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith [cos_pi, cos_three_mul (π / 3)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
⊢ cos (π / 3) = 1 / 2
have h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
Tactic: have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0 := by
    have : cos (3 * (π / 3)) = cos π := by
      congr 1
      ring
    linarith [cos_pi, cos_three_mul (π / 3)]
-- 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
⊢ cos (π / 3) = 1 / 2
have inl : ∀ (h : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0), cos (π / 3) = 1 / 2
Tactic: rcases mul_eq_zero.mp h₁ with h | h
-- 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
inl : ∀ (h : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0), cos (π / 3) = 1 / 2
⊢ cos (π / 3) = 1 / 2
have inr : ∀ (h : 2 * cos (π / 3) + 2 = 0), cos (π / 3) = 1 / 2
Tactic: rcases mul_eq_zero.mp h₁ with h | h
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
⊢ cos (π / 3) = 1 / 2
have linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₁ : cos (π / 3) < 1 / 2 → 2 / 2 = 1
Tactic: linarith [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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 [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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 [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : 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 [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
  2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
      -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
    0
Tactic: linarith [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
    2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
        -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
      0
⊢ cos (π / 3) = 1 / 2
have linarith₁₁ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
    2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
        -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
      0
linarith₁₁ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ cos (π / 3) = 1 / 2
have linarith₁₂ : 1 / 2 < cos (π / 3) → 2 / 2 = 1
Tactic: linarith [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
    2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
        -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
      0
linarith₁₁ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
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 [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
    2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
        -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
      0
linarith₁₁ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
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 [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
    2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
        -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
      0
linarith₁₁ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
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₁₅ : 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 [eq_zero_of_pow_eq_zero h]
-- 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 : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 = 0
linarith : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
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₄ : cos (π / 3) < 1 / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : cos (π / 3) < 1 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 →
    2 * cos (π / 3) - HMul.hMul (α := ℝ) 1 1 +
        -(HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
      0
linarith₁₁ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
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₁₅ : 1 / 2 < cos (π / 3) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₆ : 1 / 2 < cos (π / 3) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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 (α := ℝ) 1 1 - 2 * cos (π / 3) +
      (HMul.hMul (α := ℝ) 1 2 * (1 * cos (π / 3)) - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 0) =
    0
Tactic: linarith [eq_zero_of_pow_eq_zero h]
-- 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
⊢ cos π < cos (π / 3)
have refine_1 : 0 ≤ π / 3
Tactic: refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_
-- 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
refine_1 : 0 ≤ π / 3
⊢ cos π < cos (π / 3)
have refine_2 : π / 3 < π
Tactic: refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_
-- 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
⊢ 0 ≤ π / 3
have linarith : π / 3 < 0 → 3 / 3 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π / 3 < 0 → 3 / 3 = 1
⊢ 0 ≤ π / 3
have linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [pi_pos]
-- 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
linarith : π / 3 < 0 → 3 / 3 = 1
linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ 0 ≤ π / 3
have linarith₂ : π / 3 < 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- 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
linarith : π / 3 < 0 → 3 / 3 = 1
linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < 0 → GT.gt (α := ℝ) 3 0
⊢ 0 ≤ π / 3
have linarith₃ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π / 3 < 0 → 3 / 3 = 1
linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < 0 → GT.gt (α := ℝ) 3 0
linarith₃ linarith₄ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ 0 ≤ π / 3
have linarith₅ : π / 3 < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π / 3 < 0 → 3 / 3 = 1
linarith₁ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π / 3 < 0 → GT.gt (α := ℝ) 3 0
linarith₃ linarith₄ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : π / 3 < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : π / 3 < 0 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ 0 ≤ π / 3
have linarith₈ : π / 3 < 0 → 1 * π - HMul.hMul (α := ℝ) 3 0 + (0 - π) = 0
Tactic: linarith [pi_pos]
-- 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
⊢ π / 3 < π
have linarith : π ≤ π / 3 → 3 / 3 = 1
Tactic: linarith [pi_pos]
-- 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
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:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
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:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
linarith : π ≤ π / 3 → 3 / 3 = 1
linarith₁ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ π / 3 → GT.gt (α := ℝ) 3 0
⊢ π / 3 < π
have linarith₃ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π ≤ π / 3 → 3 / 3 = 1
linarith₁ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ linarith₄ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ π / 3 < π
have linarith₅ : π ≤ π / 3 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [pi_pos]
-- 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
linarith : π ≤ π / 3 → 3 / 3 = 1
linarith₁ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ linarith₄ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : π ≤ π / 3 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ π / 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:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
linarith : π ≤ π / 3 → 3 / 3 = 1
linarith₁ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ π / 3 → GT.gt (α := ℝ) 3 0
linarith₃ linarith₄ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : π ≤ π / 3 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₆ linarith₇ : π ≤ π / 3 → HMul.hMul (α := ℝ) 1 1 = 1
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 (hypothesis)
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2
have this : cos π < cos (π / 3)
Tactic: have : cos π < cos (π / 3) := by
      refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]