awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₁ : Eq (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
⊢ Ne (α := ℝ) 2 0

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Premises used: le_rfl, Real.sqrtTwoAddSeries_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₁ : π / HPow.hPow (α := ℝ) 2 (n + 1) < -π → GT.gt (α := ℝ) 2 0
⊢ -π ≤ π / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Premises used: le_rfl, Real.sqrtTwoAddSeries_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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 * π + (1 * π - 1 * (π / HPow.hPow (α := ℝ) 2 (n + 1))) = 0
⊢ π / HPow.hPow (α := ℝ) 2 (n + 1) ≤ π

Tactic:
linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Premises used: le_rfl, Real.sqrtTwoAddSeries_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
rw :
  1 - HPow.hPow (β := ℕ) (cos (π / HPow.hPow (α := ℝ) 2 (n + 1))) 2 =
    1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 2
rw₁ rw₂ : 1 - HPow.hPow (β := ℕ) (sqrtTwoAddSeries 0 n / 2) 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

Tactic:
rw [sin_sq, cos_pi_over_two_pow]

Premises used: Real.sin_sq, Real.cos_pi_over_two_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
rw :
  1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / HPow.hPow (α := ℝ) (β := ℕ) 2 2 =
    1 / 2 - sqrtTwoAddSeries 0 n / 4
rw₁ : 0 ≤ 2 + sqrtTwoAddSeries 0 n
⊢ HPow.hPow (β := ℕ) (sin (π / HPow.hPow (α := ℝ) 2 (n + 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]

Premises used: Real.sq_sqrt, sub_sub, Real.sqrtTwoAddSeries, div_pow, Real.sin_sq_pi_over_two_pow, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
e_a : 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 1 / 2
e_a₁ : HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 4
⊢ 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / HPow.hPow (α := ℝ) (β := ℕ) 2 2 =
    1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 1 - 2 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 4

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)

Premises used: two_pos, LT.lt.le, add_nonneg, Real.sqrtTwoAddSeries_zero_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)

Premises used: two_pos, LT.lt.le, add_nonneg, Real.sqrtTwoAddSeries_zero_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
hy : 0 ≤ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) * 2
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 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]

Premises used: Real.sqrt_eq_iff_eq_sq, eq_comm, sub_mul, two_ne_zero, eq_div_iff_mul_eq, mul_pow, Real.sin_sq_pi_over_two_pow_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
e_a : 2 = 1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
e_a₁ : sqrtTwoAddSeries 0 n = sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ 2 - sqrtTwoAddSeries 0 n =
    1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 - sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 2 = 1 / 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 n = sqrtTwoAddSeries 0 n / 4 * HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
hx : sqrtTwoAddSeries 0 n ≤ 2
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2

Tactic:
(sqrtTwoAddSeries_lt_two _).le

Premises used: LT.lt.le, Real.sqrtTwoAddSeries_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2

Tactic:
exact (sqrtTwoAddSeries_lt_two _).le

Premises used: LT.lt.le, Real.sqrtTwoAddSeries_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 0 ≤ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) * 2

Tactic:
mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two

Premises used: mul_nonneg, Real.sin_nonneg_of_nonneg_of_le_pi, zero_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
hy : 0 ≤ π / HPow.hPow (α := ℝ) 2 (n + 2)
hy₁ : π / HPow.hPow (α := ℝ) 2 (n + 2) ≤ π
⊢ 0 ≤ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) * 2

Tactic:
refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two

Premises used: mul_nonneg, Real.sin_nonneg_of_nonneg_of_le_pi, zero_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ 0 ≤ π / HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ π / HPow.hPow (α := ℝ) 2 (n + 2) ≤ π

Tactic:
div_le_self pi_pos.le <| one_le_pow₀ one_le_two

Premises used: one_le_pow₀, Real.pi_pos, LT.lt.le, div_le_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ π / HPow.hPow (α := ℝ) 2 (n + 2) ≤ π

Tactic:
exact div_le_self pi_pos.le <| one_le_pow₀ one_le_two

Premises used: one_le_pow₀, Real.pi_pos, LT.lt.le, div_le_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : cos (π / 4) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2) = √2 / 2
⊢ cos (π / 4) = √2 / 2

Tactic:
trans cos (π / 2 ^ 2)

Premises used: Real.pi, Real.cos, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ cos (π / 4) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2) = √2 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : sin (π / 4) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)
trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2) = √2 / 2
⊢ sin (π / 4) = √2 / 2

Tactic:
trans sin (π / 2 ^ 2)

Premises used: Real.pi, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2
⊢ sin (π / 4) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 2) = √2 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : cos (π / 8) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3) = √(2 + √2) / 2
⊢ cos (π / 8) = √(2 + √2) / 2

Tactic:
trans cos (π / 2 ^ 3)

Premises used: Real.pi, Real.cos, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 8 = HPow.hPow (α := ℝ) (β := ℕ) 2 3
⊢ cos (π / 8) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 8 = HPow.hPow (α := ℝ) (β := ℕ) 2 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3) = √(2 + √2) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : sin (π / 8) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)
trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3) = √(2 - √2) / 2
⊢ sin (π / 8) = √(2 - √2) / 2

Tactic:
trans sin (π / 2 ^ 3)

Premises used: Real.pi, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 8 = HPow.hPow (α := ℝ) (β := ℕ) 2 3
⊢ sin (π / 8) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 3) = √(2 - √2) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : cos (π / 16) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4) = √(2 + √(2 + √2)) / 2
⊢ cos (π / 16) = √(2 + √(2 + √2)) / 2

Tactic:
trans cos (π / 2 ^ 4)

Premises used: Real.pi, Real.cos, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 16 = HPow.hPow (α := ℝ) (β := ℕ) 2 4
⊢ cos (π / 16) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 16 = HPow.hPow (α := ℝ) (β := ℕ) 2 4

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4) = √(2 + √(2 + √2)) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : sin (π / 16) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)
trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4) = √(2 - √(2 + √2)) / 2
⊢ sin (π / 16) = √(2 - √(2 + √2)) / 2

Tactic:
trans sin (π / 2 ^ 4)

Premises used: Real.pi, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 16 = HPow.hPow (α := ℝ) (β := ℕ) 2 4
⊢ sin (π / 16) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 4) = √(2 - √(2 + √2)) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : cos (π / 32) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
trans₁ : cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5) = √(2 + √(2 + √(2 + √2))) / 2
⊢ cos (π / 32) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
trans cos (π / 2 ^ 5)

Premises used: Real.pi, Real.cos, HDiv.hDiv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 32 = HPow.hPow (α := ℝ) (β := ℕ) 2 5
⊢ cos (π / 32) = cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 32 = HPow.hPow (α := ℝ) (β := ℕ) 2 5

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
trans : sin (π / 32) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)
trans₁ : sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5) = √(2 - √(2 + √(2 + √2))) / 2
⊢ sin (π / 32) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
trans sin (π / 2 ^ 5)

Premises used: Real.pi, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 32 = HPow.hPow (α := ℝ) (β := ℕ) 2 5
⊢ sin (π / 32) = sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ sin (π / HPow.hPow (α := ℝ) (β := ℕ) 2 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : 3 * (π / 3) = π
⊢ cos (3 * (π / 3)) = cos π

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 3 * (π / 3) = π

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cos (3 * (π / 3)) = cos π

Tactic:
have : cos (3 * (π / 3)) = cos π := by
      congr 1
      ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₁₉ linarith₂₀ linarith₂₁ :
  0 < HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) → GT.gt (α := ℝ) 2 0
⊢ HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0

Tactic:
linarith [cos_pi, cos_three_mul (π / 3)]

Premises used: Real.pi, Real.cos_three_mul, HDiv.hDiv, OfNat.ofNat, Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 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)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
inr : ∀ (h : 2 * cos (π / 3) + 2 = 0), cos (π / 3) = 1 / 2
⊢ cos (π / 3) = 1 / 2

Tactic:
rcases mul_eq_zero.mp h₁ with h | h

Premises used: mul_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
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
⊢ cos (π / 3) = 1 / 2

Tactic:
linarith [eq_zero_of_pow_eq_zero h]

Premises used: eq_zero_of_pow_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos π < cos (π / 3)

Tactic:
cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_

Premises used: le_rfl, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
refine_1 : 0 ≤ π / 3
refine_2 : π / 3 < π
⊢ cos π < cos (π / 3)

Tactic:
refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_

Premises used: le_rfl, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₈ : π / 3 < 0 → 1 * π - HMul.hMul (α := ℝ) 3 0 + (0 - π) = 0
⊢ 0 ≤ π / 3

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₉ : π ≤ π / 3 → GT.gt (α := ℝ) 2 0
⊢ π / 3 < π

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h₁ : HPow.hPow (β := ℕ) (2 * cos (π / 3) - 1) 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos π < cos (π / 3)

Tactic:
have : cos π < cos (π / 3) := by
      refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₂₀ : 1 / 2 < cos (π / 3) → GT.gt (α := ℝ) 3 0
⊢ cos (π / 3) = 1 / 2

Tactic:
linarith [cos_pi]

Premises used: Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 6 = HMul.hMul (α := ℝ) 3 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : LE.le (α := ℝ) 0 2
hx : LE.le (α := ℝ) 0 3
rw₁ : Ne (α := ℝ) 2 0
hl : -π ≤ π / 3
hr : π / 3 ≤ π
⊢ cos (π / 6) = √3 / 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]

Premises used: Real.sqrt_mul_self, Real.cos_half, one_add_div, Real.sqrt_div, div_mul_eq_div_div, two_add_one_eq_three, Real.cos_pi_div_three
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
linarith₁ : LT.lt (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
⊢ LE.le (α := ℝ) 0 2

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
linarith : LT.lt (α := ℝ) 3 0 → HMul.hMul (α := ℝ) 3 (-1) + HSub.hSub (α := ℝ) 3 0 = 0
linarith₁ : LT.lt (α := ℝ) 3 0 → GT.gt (α := ℝ) 3 0
⊢ LE.le (α := ℝ) 0 3

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
linarith : Eq (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
linarith₁ : Eq (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
⊢ Ne (α := ℝ) 2 0

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₄ : π / 3 < -π → GT.gt (α := ℝ) 4 0
⊢ -π ≤ π / 3

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos