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
calc : s * (2 * c) = 2 * s * c
calc₁ : 2 * s * c = sin (2 * θ)
calc₂ : sin (2 * θ) = sin (π - 2 * θ)
calc₃ : sin (π - 2 * θ) = sin (2 * θ + θ)
calc₄ : sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₅ : 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * 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
-- 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 * θ + θ)
calc₄ : sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
calc₅ : 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₆ : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
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 * θ + θ)
calc₄ : sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
calc₅ : 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s
calc₆ : 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)
⊢ s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
have calc₇ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
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:
c : ℝ := cos (π / 5)
⊢ 4 * (c * c) + -2 * c + -1 = 0
have rw : 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0
Tactic: rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
c : ℝ := cos (π / 5)
⊢ c = (1 + √5) / 4
have this : 4 * (c * c) + -2 * c + -1 = 0
Tactic: have : 4 * (c * c) + (-2) * c + (-1) = 0 := by
    rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]
    exact quadratic_root_cos_pi_div_five
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ c = (1 + √5) / 4
have hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
Tactic: have hd : discrim 4 (-2) (-1) = (2 * √5) * (2 * √5) := by norm_num [discrim, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ c = (1 + √5) / 4
have inl : ∀ (h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4), c = (1 + √5) / 4
Tactic: rcases (quadratic_eq_zero_iff (by simp) hd c).mp this with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
inl : ∀ (h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4), c = (1 + √5) / 4
⊢ c = (1 + √5) / 4
have inr : ∀ (h : c = (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4), c = (1 + √5) / 4
Tactic: rcases (quadratic_eq_zero_iff (by simp) hd c).mp this with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
⊢ c = (1 + √5) / 4
have inl : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₀ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
  HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₂ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 2 4 = 8
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
linarith₁₂ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 2 4 = 8
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₃ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
linarith₁₂ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₁₃ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₄ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 8 / 8 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
linarith₁₂ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₁₃ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₄ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 8 / 8 = 1
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₅ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 8 = 8
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
linarith₁₂ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₁₃ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₄ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 8 / 8 = 1
linarith₁₅ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 8 = 8
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₁₆ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → GT.gt (α := ℝ) 8 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4
linarith : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₂ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₃ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 4 / 4 = 1
linarith₄ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₅ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₆ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → 8 / 8 = 1
linarith₈ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₉ : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 → GT.gt (α := ℝ) 8 0
linarith₁₀ :
  (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 < (1 + √5) / 4 →
    HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5) - (HMul.hMul (α := ℝ) 2 1 + 2 * √5) = 0
linarith₁₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 4 / 4 = 1
linarith₁₂ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 2 4 = 8
linarith₁₃ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₄ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 8 / 8 = 1
linarith₁₅ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₁₆ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → GT.gt (α := ℝ) 8 0
linarith₁₇ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₈ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → 8 / 8 = 1
linarith₁₉ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₂₀ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 → GT.gt (α := ℝ) 8 0
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
have linarith₂₁ : (1 + √5) / 4 < (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 →
  HMul.hMul (α := ℝ) 2 1 + 2 * √5 - (HMul.hMul (α := ℝ) 1 2 + HMul.hMul (α := ℝ) 1 2 * (1 * √5)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4
⊢ π / 5 ∈ Icc (-(π / 2)) (π / 2)
have left : -(π / 2) ≤ π / 5
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4
left : -(π / 2) ≤ π / 5
⊢ π / 5 ∈ Icc (-(π / 2)) (π / 2)
have right : π / 5 ≤ π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4
⊢ -(π / 2) ≤ π / 5
have linarith : π / 5 < -(π / 2) → 5 / 5 = 1
Tactic: linarith [pi_pos.le]