awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ Ne (α := ℝ) 2 0
have linarith : Eq (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
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 [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ -π ≤ π / HPow.hPow (α := ℝ) 2 (n + 1)
have linarith : π / HPow.hPow (α := ℝ) 2 (n + 1) < -π →
  1 * (π / HPow.hPow (α := ℝ) 2 (n + 1)) - 1 * π +
        2 * (HMul.hMul (α := ℝ) 1 0 - 1 * (π / HPow.hPow (α := ℝ) 2 (n + 1))) +
      (1 * (π / HPow.hPow (α := ℝ) 2 (n + 1)) - -(1 * π)) =
    0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
linarith :
  π / HPow.hPow (α := ℝ) 2 (n + 1) < -π →
    1 * (π / HPow.hPow (α := ℝ) 2 (n + 1)) - 1 * π +
          2 * (HMul.hMul (α := ℝ) 1 0 - 1 * (π / HPow.hPow (α := ℝ) 2 (n + 1))) +
        (1 * (π / HPow.hPow (α := ℝ) 2 (n + 1)) - -(1 * π)) =
      0
⊢ -π ≤ π / HPow.hPow (α := ℝ) 2 (n + 1)
have linarith₁ : π / HPow.hPow (α := ℝ) 2 (n + 1) < -π → GT.gt (α := ℝ) 2 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ π / HPow.hPow (α := ℝ) 2 (n + 1) ≤ π
have linarith : π < π / HPow.hPow (α := ℝ) 2 (n + 1) →
  1 * (π / HPow.hPow (α := ℝ) 2 (n + 1)) - 1 * π + (1 * π - 1 * (π / HPow.hPow (α := ℝ) 2 (n + 1))) = 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (sin (π / HPow.hPow (α := ℝ) 2 (n + 1))) 2 = 1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2
have rw : 1 - HPow.hPow (β := ℕ) (cos (π / HPow.hPow (α := ℝ) 2 (n + 1))) 2 = 1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2
Tactic: rw [sin_sq, cos_pi_over_two_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
rw :
  1 - HPow.hPow (β := ℕ) (cos (π / HPow.hPow (α := ℝ) 2 (n + 1))) 2 =
    1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2
⊢ HPow.hPow (β := ℕ) (sin (π / HPow.hPow (α := ℝ) 2 (n + 1))) 2 = 1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2
have rw₁ : 1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2 = 1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2
Tactic: rw [sin_sq, cos_pi_over_two_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (sin (π / HPow.hPow (α := ℝ) 2 (n + 2))) 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
have rw : 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / HPow.hPow (α := ℝ) (β := ℕ) 2 2 =
  1 / 2 - sqrtTwoAddSeries 0 n / 4
Tactic: rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
rw :
  1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / HPow.hPow (α := ℝ) (β := ℕ) 2 2 =
    1 / 2 - sqrtTwoAddSeries 0 n / 4
⊢ HPow.hPow (β := ℕ) (sin (π / HPow.hPow (α := ℝ) 2 (n + 2))) 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
have rw₁ : 0 ≤ 2 + sqrtTwoAddSeries 0 n
Tactic: rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / HPow.hPow (α := ℝ) (β := ℕ) 2 2 =
    1 / 2 - sqrtTwoAddSeries 0 n / 4
have e_a : 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 1 / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
e_a : 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 1 / 2
⊢ 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / HPow.hPow (α := ℝ) (β := ℕ) 2 2 =
    1 / 2 - sqrtTwoAddSeries 0 n / 4
have e_a₁ : HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 4
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2
have rw : 2 - sqrtTwoAddSeries 0 n =
  1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow,
    sin_sq_pi_over_two_pow_succ, sub_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
rw :
  2 - sqrtTwoAddSeries 0 n =
    1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2
have hx : 0 ≤ 2 - sqrtTwoAddSeries 0 n
Tactic: rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow,
    sin_sq_pi_over_two_pow_succ, sub_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
rw :
  2 - sqrtTwoAddSeries 0 n =
    1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
hx : 0 ≤ 2 - sqrtTwoAddSeries 0 n
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2
have hy : 0 ≤ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) * 2
Tactic: rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow,
    sin_sq_pi_over_two_pow_succ, sub_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n =
    1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
have e_a : 2 = 1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
e_a : 2 = 1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ 2 - sqrtTwoAddSeries 0 n =
    1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
have e_a₁ : sqrtTwoAddSeries 0 n = sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n
have hx : sqrtTwoAddSeries 0 n ≤ 2
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ 0 ≤ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) * 2
have hy : 0 ≤ π / HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
hy : 0 ≤ π / HPow.hPow (α := ℝ) 2 (n + 2)
⊢ 0 ≤ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) * 2
have hy₁ : π / HPow.hPow (α := ℝ) 2 (n + 2) ≤ π
Tactic: refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 4) = √2 / 2
have trans : cos (π / 4) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
Tactic: trans cos (π / 2 ^ 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : cos (π / 4) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
⊢ cos (π / 4) = √2 / 2
have trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2) = √2 / 2
Tactic: trans cos (π / 2 ^ 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 4) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
have e_x : 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 4) = √2 / 2
have trans : sin (π / 4) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
Tactic: trans sin (π / 2 ^ 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : sin (π / 4) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
⊢ sin (π / 4) = √2 / 2
have trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2) = √2 / 2
Tactic: trans sin (π / 2 ^ 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 4) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
have e_x : 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 8) = √(2 + √2) / 2
have trans : cos (π / 8) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
Tactic: trans cos (π / 2 ^ 3)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : cos (π / 8) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
⊢ cos (π / 8) = √(2 + √2) / 2
have trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3) = √(2 + √2) / 2
Tactic: trans cos (π / 2 ^ 3)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 8) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
have e_x : 8 = HPow.hPow (α := ℝ) (β := ℕ) 2 3
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 8) = √(2 - √2) / 2
have trans : sin (π / 8) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
Tactic: trans sin (π / 2 ^ 3)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : sin (π / 8) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
⊢ sin (π / 8) = √(2 - √2) / 2
have trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3) = √(2 - √2) / 2
Tactic: trans sin (π / 2 ^ 3)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 8) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
have e_x : 8 = HPow.hPow (α := ℝ) (β := ℕ) 2 3
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 16) = √(2 + √(2 + √2)) / 2
have trans : cos (π / 16) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
Tactic: trans cos (π / 2 ^ 4)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : cos (π / 16) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
⊢ cos (π / 16) = √(2 + √(2 + √2)) / 2
have trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4) = √(2 + √(2 + √2)) / 2
Tactic: trans cos (π / 2 ^ 4)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 16) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
have e_x : 16 = HPow.hPow (α := ℝ) (β := ℕ) 2 4
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 16) = √(2 - √(2 + √2)) / 2
have trans : sin (π / 16) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
Tactic: trans sin (π / 2 ^ 4)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : sin (π / 16) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
⊢ sin (π / 16) = √(2 - √(2 + √2)) / 2
have trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4) = √(2 - √(2 + √2)) / 2
Tactic: trans sin (π / 2 ^ 4)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 16) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
have e_x : 16 = HPow.hPow (α := ℝ) (β := ℕ) 2 4
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 32) = √(2 + √(2 + √(2 + √2))) / 2
have trans : cos (π / 32) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
Tactic: trans cos (π / 2 ^ 5)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : cos (π / 32) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
⊢ cos (π / 32) = √(2 + √(2 + √(2 + √2))) / 2
have trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5) = √(2 + √(2 + √(2 + √2))) / 2
Tactic: trans cos (π / 2 ^ 5)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 32) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
have e_x : 32 = HPow.hPow (α := ℝ) (β := ℕ) 2 5
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 32) = √(2 - √(2 + √(2 + √2))) / 2
have trans : sin (π / 32) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
Tactic: trans sin (π / 2 ^ 5)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
trans : sin (π / 32) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
⊢ sin (π / 32) = √(2 - √(2 + √(2 + √2))) / 2
have trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5) = √(2 - √(2 + √(2 + √2))) / 2
Tactic: trans sin (π / 2 ^ 5)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (π / 32) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
have e_x : 32 = HPow.hPow (α := ℝ) (β := ℕ) 2 5
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (3 * (π / 3)) = cos π
have e_x : 3 * (π / 3) = π
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have this : cos (3 * (π / 3)) = cos π
Tactic: have : cos (3 * (π / 3)) = cos π := by
      congr 1
      ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
this : cos (3 * (π / 3)) = cos π
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have linarith : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
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
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have linarith₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → HMul.hMul (α := ℝ) 1 1 = 1
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
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have linarith₄ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
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
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have 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
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
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
have linarith₈ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) < 0 → GT.gt (α := ℝ) 2 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
⊢ 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) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
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
⊢ 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) → HMul.hMul (α := ℝ) 1 1 = 1
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
⊢ 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) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith [cos_pi, cos_three_mul (π / 3)]