awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
⊢ π - 2 * θ = 2 * θ + θ
have linarith₂ : π - 2 * θ < 2 * θ + θ → GT.gt (α := ℝ) 5 0
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
linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ : π - 2 * θ < 2 * θ + θ → GT.gt (α := ℝ) 5 0
⊢ π - 2 * θ = 2 * θ + θ
have linarith₃ : π - 2 * θ < 2 * θ + θ → 5 * θ - 1 * π + (π - 2 * θ - (2 * θ + θ)) = 0
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
linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ : π - 2 * θ < 2 * θ + θ → GT.gt (α := ℝ) 5 0
linarith₃ : π - 2 * θ < 2 * θ + θ → 5 * θ - 1 * π + (π - 2 * θ - (2 * θ + θ)) = 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
linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ : π - 2 * θ < 2 * θ + θ → GT.gt (α := ℝ) 5 0
linarith₃ : π - 2 * θ < 2 * θ + θ → 5 * θ - 1 * π + (π - 2 * θ - (2 * θ + θ)) = 0
linarith₄ : 2 * θ + θ < π - 2 * θ → 5 / 5 = 1
⊢ π - 2 * θ = 2 * θ + θ
have linarith₅ : 2 * θ + θ < π - 2 * θ → HMul.hMul (α := ℝ) 1 5 = 5
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
linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ : π - 2 * θ < 2 * θ + θ → GT.gt (α := ℝ) 5 0
linarith₃ : π - 2 * θ < 2 * θ + θ → 5 * θ - 1 * π + (π - 2 * θ - (2 * θ + θ)) = 0
linarith₄ : 2 * θ + θ < π - 2 * θ → 5 / 5 = 1
linarith₅ : 2 * θ + θ < π - 2 * θ → HMul.hMul (α := ℝ) 1 5 = 5
⊢ π - 2 * θ = 2 * θ + θ
have linarith₆ : 2 * θ + θ < π - 2 * θ → GT.gt (α := ℝ) 5 0
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
linarith₁ : π - 2 * θ < 2 * θ + θ → HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ : π - 2 * θ < 2 * θ + θ → GT.gt (α := ℝ) 5 0
linarith₃ : π - 2 * θ < 2 * θ + θ → 5 * θ - 1 * π + (π - 2 * θ - (2 * θ + θ)) = 0
linarith₄ : 2 * θ + θ < π - 2 * θ → 5 / 5 = 1
linarith₅ : 2 * θ + θ < π - 2 * θ → HMul.hMul (α := ℝ) 1 5 = 5
linarith₆ : 2 * θ + θ < π - 2 * θ → GT.gt (α := ℝ) 5 0
⊢ π - 2 * θ = 2 * θ + θ
have linarith₇ : 2 * θ + θ < π - 2 * θ → -(5 * θ - 1 * π) + (2 * θ + θ - (π - 2 * θ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
have rw : 2 * sin θ * cos θ * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
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
⊢ 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s
have rw : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) (cos θ) 2 - 1) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s
Tactic: rw [cos_two_mul]
-- 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 * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
  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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₁ : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
  HMul.hMul (α := ℝ) 1 5 = 5
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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
linarith₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₂ : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
  GT.gt (α := ℝ) 5 0
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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
linarith₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    GT.gt (α := ℝ) 5 0
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₃ : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s - (s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)) = 0
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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
linarith₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    GT.gt (α := ℝ) 5 0
linarith₃ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s - (s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)) = 0
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₄ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
  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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
linarith₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    GT.gt (α := ℝ) 5 0
linarith₃ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s - (s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)) = 0
linarith₄ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
    5 / 5 = 1
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₅ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
  HMul.hMul (α := ℝ) 1 5 = 5
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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
linarith₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    GT.gt (α := ℝ) 5 0
linarith₃ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s - (s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)) = 0
linarith₄ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
    5 / 5 = 1
linarith₅ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
    HMul.hMul (α := ℝ) 1 5 = 5
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₆ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
  GT.gt (α := ℝ) 5 0
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 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    5 / 5 = 1
linarith₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    GT.gt (α := ℝ) 5 0
linarith₃ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s - (s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)) = 0
linarith₄ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
    5 / 5 = 1
linarith₅ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₆ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
    GT.gt (α := ℝ) 5 0
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₇ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s →
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) - (2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s) = 0
Tactic: linarith
-- 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 * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₁ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
  HMul.hMul (α := ℝ) 1 5 = 5
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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₁ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₂ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₁ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₃ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) - s * (4 * HPow.hPow (β := ℕ) c 2 - 1) = 0
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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₁ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
linarith₃ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) - s * (4 * HPow.hPow (β := ℕ) c 2 - 1) = 0
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₄ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) → 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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₁ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
linarith₃ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) - s * (4 * HPow.hPow (β := ℕ) c 2 - 1) = 0
linarith₄ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₅ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
  HMul.hMul (α := ℝ) 1 5 = 5
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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₁ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
linarith₃ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) - s * (4 * HPow.hPow (β := ℕ) c 2 - 1) = 0
linarith₄ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₅ :
  s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₆ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
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 : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₁ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₂ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
linarith₃ :
  s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) < s * (4 * HPow.hPow (β := ℕ) c 2 - 1) →
    s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) - s * (4 * HPow.hPow (β := ℕ) c 2 - 1) = 0
linarith₄ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) → 5 / 5 = 1
linarith₅ :
  s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
    HMul.hMul (α := ℝ) 1 5 = 5
linarith₆ :
  s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) → GT.gt (α := ℝ) 5 0
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have linarith₇ : s * (4 * HPow.hPow (β := ℕ) c 2 - 1) < s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) →
  s * (4 * HPow.hPow (β := ℕ) c 2 - 1) - (s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)) = 0
Tactic: linarith
-- 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) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc : s * (2 * c) = 2 * s * c
Tactic: calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
calc : s * (2 * c) = 2 * s * c
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₁ : 2 * s * c = sin (2 * θ)
Tactic: calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
calc : s * (2 * c) = 2 * s * c
calc₁ : 2 * s * c = sin (2 * θ)
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₂ : sin (2 * θ) = sin (π - 2 * θ)
Tactic: calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
calc : s * (2 * c) = 2 * s * c
calc₁ : 2 * s * c = sin (2 * θ)
calc₂ : sin (2 * θ) = sin (π - 2 * θ)
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₃ : sin (π - 2 * θ) = sin (2 * θ + θ)
Tactic: calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
calc : s * (2 * c) = 2 * s * c
calc₁ : 2 * s * c = sin (2 * θ)
calc₂ : sin (2 * θ) = sin (π - 2 * θ)
calc₃ : sin (π - 2 * θ) = sin (2 * θ + θ)
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₄ : sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
Tactic: calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith