awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → 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:
rw : 3 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 3 / 4
rw₁ : LE.le (α := ℝ) 0 3
⊢ HPow.hPow (β := ℕ) (cos (π / 6)) 2 = 3 / 4

Tactic:
rw [cos_pi_div_six, div_pow, sq_sqrt]

Premises used: Real.sq_sqrt, Real.cos_pi_div_six, div_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 3 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 = 3 / 4

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ LE.le (α := ℝ) 0 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : cos (π / 2 - π / 6) = cos (π / 3)
⊢ sin (π / 6) = 1 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_three]

Premises used: Real.cos_pi_div_three, Real.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : π / 2 - π / 6 = π / 3
⊢ cos (π / 2 - π / 6) = cos (π / 3)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ π / 2 - π / 6 = π / 3

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : HPow.hPow (β := ℕ) (cos (π / 2 - π / 3)) 2 = HPow.hPow (β := ℕ) (cos (π / 6)) 2
⊢ HPow.hPow (β := ℕ) (sin (π / 3)) 2 = 3 / 4

Tactic:
rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]

Premises used: Real.sq_cos_pi_div_six, Real.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_a : π / 2 - π / 3 = π / 6
⊢ HPow.hPow (β := ℕ) (cos (π / 2 - π / 3)) 2 = HPow.hPow (β := ℕ) (cos (π / 6)) 2

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ π / 2 - π / 3 = π / 6

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : cos (π / 2 - π / 3) = cos (π / 6)
⊢ sin (π / 3) = √3 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_six]

Premises used: Real.cos_pi_div_six, Real.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
e_x : π / 2 - π / 3 = π / 6
⊢ cos (π / 2 - π / 3) = cos (π / 6)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
set :
  let θ := π / 5;
  ∀ (hθ : θ = π / 5), 4 * HPow.hPow (β := ℕ) (cos θ) 2 - 2 * cos θ - 1 = 0
⊢ 4 * HPow.hPow (β := ℕ) (cos (π / 5)) 2 - 2 * cos (π / 5) - 1 = 0

Tactic:
set θ := π / 5 with hθ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
set :
  let c := cos θ;
  4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0
⊢ 4 * HPow.hPow (β := ℕ) (cos θ) 2 - 2 * cos θ - 1 = 0

Tactic:
set c := cos θ

Premises used: Real.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
this : 2 * c = 4 * HPow.hPow (β := ℕ) c 2 - 1
⊢ 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
suffices : 2 * c = 4 * HPow.hPow (β := ℕ) c 2 - 1
⊢ 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0

Tactic:
suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
rw : ¬∃ (n : ℤ), (↑n : ℝ) * π = π / 5
⊢ s ≠ 0

Tactic:
rw [ne_eq, sin_eq_zero_iff, hθ]

Premises used: ne_eq, Real.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
push : ∀ (n : ℤ), (↑n : ℝ) * π ≠ π / 5
⊢ ¬∃ (n : ℤ), (↑n : ℝ) * π = π / 5

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : (↑n : ℝ) * π = π / 5
⊢ HMul.hMul (α := ℝ) (↑n : ℝ) 5 = 1

Tactic:
field_simp at hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : HMul.hMul (α := ℝ) (↑n : ℝ) 5 = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (hn : n * 5 = 1), n * 5 = 1
⊢ n * 5 = 1

Tactic:
norm_cast at hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : (↑n : ℝ) * π = π / 5
⊢ n * 5 = 1

Tactic:
replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : n * 5 = 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ s ≠ 0

Tactic:
have hs : s ≠ 0 := by
    rw [ne_eq, sin_eq_zero_iff, hθ]
    push Not
    intro n hn
    replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
    lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
suffices : s * (2 * c) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
⊢ 2 * c = 4 * HPow.hPow (β := ℕ) c 2 - 1

Tactic:
suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
rw : s * 2 * c = 2 * s * c
rw₁ rw₂ : s * 2 * c = s * 2 * c
⊢ s * (2 * c) = 2 * s * c

Tactic:
rw [← mul_assoc, mul_comm 2]

Premises used: mul_assoc, mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
rw rw₁ : 2 * s * c = 2 * sin θ * cos θ
⊢ 2 * s * c = sin (2 * θ)

Tactic:
rw [sin_two_mul]

Premises used: Real.sin_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
rw rw₁ : sin (2 * θ) = sin (2 * θ)
⊢ sin (2 * θ) = sin (π - 2 * θ)

Tactic:
rw [sin_pi_sub]

Premises used: Real.sin_pi_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
e_x : π - 2 * θ = 2 * θ + θ
⊢ sin (π - 2 * θ) = sin (2 * θ + θ)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
linarith₇ : 2 * θ + θ < π - 2 * θ → -(5 * θ - 1 * π) + (2 * θ + θ - (π - 2 * θ)) = 0
⊢ π - 2 * θ = 2 * θ + θ

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ + θ) = sin (2 * θ) * c + cos (2 * θ) * s

Tactic:
sin_add (2 * θ) θ

Premises used: HMul.hMul, Real.sin_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
rw rw₁ : 2 * sin θ * cos θ * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
⊢ sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s

Tactic:
rw [sin_two_mul]

Premises used: Real.sin_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
rw rw₁ :
  2 * s * c * c + (2 * HPow.hPow (β := ℕ) (cos θ) 2 - 1) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s
⊢ 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s

Tactic:
rw [cos_two_mul]

Premises used: Real.cos_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
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
⊢ 2 * s * c * c + (2 * HPow.hPow (β := ℕ) c 2 - 1) * s = s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
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
⊢ s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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)
calc₇ : s * (2 * c * c) + s * (2 * HPow.hPow (β := ℕ) c 2 - 1) = s * (4 * HPow.hPow (β := ℕ) c 2 - 1)
⊢ s * (2 * c) = 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

Premises used: Real.pi, HMul.hMul, Real.cos, HSub.hSub, Real.sin_add, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ (HSMul.hSMul (α := ℕ) 4 (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2) - HSMul.hSMul (α := ℕ) (β := ℝ[X]) 2 X -
        (C : (a : ℝ) → ℝ[X]) 1).IsRoot
    (cos (π / 5))

Tactic:
simpa using quadratic_root_cos_pi_div_five

Premises used: Real.quadratic_root_cos_pi_div_five
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
set :
  let c := cos (π / 5);
  c = (1 + √5) / 4
⊢ cos (π / 5) = (1 + √5) / 4

Tactic:
set c := cos (π / 5)

Premises used: Real.pi, Real.cos, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
rw : 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0
⊢ 4 * (c * c) + -2 * c + -1 = 0

Tactic:
rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, sq, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
⊢ 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0

Tactic:
quadratic_root_cos_pi_div_five

Premises used: Real.quadratic_root_cos_pi_div_five
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
⊢ 4 * HPow.hPow (β := ℕ) c 2 - 2 * c - 1 = 0

Tactic:
exact quadratic_root_cos_pi_div_five

Premises used: Real.quadratic_root_cos_pi_div_five
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)

Tactic:
norm_num [discrim, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, discrim
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
⊢ Ne (α := ℝ) 4 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
inr : ∀ (h : c = (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4), c = (1 + √5) / 4
⊢ c = (1 + √5) / 4

Tactic:
rcases (quadratic_eq_zero_iff (by simp) hd c).mp this with h | h

Premises used: quadratic_eq_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
inl : (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4
⊢ c = (1 + √5) / 4

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
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
⊢ (2 + 2 * √5) / HMul.hMul (α := ℝ) 2 4 = (1 + √5) / 4

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
right : π / 5 ≤ π / 2
⊢ π / 5 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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 : π / 5 < -(π / 2) → 5 / 5 = 1
linarith₁ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : π / 5 < -(π / 2) → 2 / 2 = 1
linarith₃ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 5 2 = 10
linarith₄ : π / 5 < -(π / 2) → GT.gt (α := ℝ) 10 0
linarith₅ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₆ : π / 5 < -(π / 2) → 8 / 8 = 1
linarith₇ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 1 8 = 8
linarith₈ : π / 5 < -(π / 2) → GT.gt (α := ℝ) 8 0
linarith₉ : π / 5 < -(π / 2) → 2 * π - -(5 * π) + 7 * (0 - π) = 0
linarith₁₀ : π / 5 < -(π / 2) → GT.gt (α := ℝ) 7 0
⊢ -(π / 2) ≤ π / 5

Tactic:
linarith [pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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 < π / 5 → 2 / 2 = 1
linarith₁ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 5 2 = 10
linarith₂ : π / 2 < π / 5 → 5 / 5 = 1
linarith₃ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 2 5 = 10
linarith₄ : π / 2 < π / 5 → GT.gt (α := ℝ) 10 0
linarith₅ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₆ : π / 2 < π / 5 → 8 / 8 = 1
linarith₇ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 1 8 = 8
linarith₈ : π / 2 < π / 5 → GT.gt (α := ℝ) 8 0
linarith₉ : π / 2 < π / 5 → 5 * π - 2 * π + 3 * (0 - π) = 0
linarith₁₀ : π / 2 < π / 5 → GT.gt (α := ℝ) 3 0
⊢ π / 5 ≤ π / 2

Tactic:
linarith [pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
inr : ¬0 ≤ c
⊢ c = (1 + √5) / 4

Tactic:
absurd (show 0 ≤ c from cos_nonneg_of_mem_Icc <| by constructor <;> linarith [pi_pos.le])

Premises used: Real.cos_nonneg_of_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
inr : (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4 < 0
⊢ ¬0 ≤ c

Tactic:
rw [not_le, h]

Premises used: not_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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 < 0

Tactic:
norm_num [lt_sqrt]

Premises used: Real.lt_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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
⊢ 0 < HMul.hMul (α := ℝ) 2 4

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
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 < 0

Tactic:
exact div_neg_of_neg_of_pos (by norm_num [lt_sqrt]) (by positivity)

Premises used: div_neg_of_neg_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : (↑(Icc (-(π / 2)) (π / 2)) : Type)
⊢ (↑((sinOrderIso : (a : (↑(Icc (-(π / 2)) (π / 2)) : Type)) → (↑(Icc (-1) 1) : Type)) x) : ℝ) = sin (↑x : ℝ)

Tactic:
rfl

Premises used: Real.sin, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : (↑(Icc (-(π / 2)) (π / 2)) : Type)
⊢ (sinOrderIso : (a : (↑(Icc (-(π / 2)) (π / 2)) : Type)) → (↑(Icc (-1) 1) : Type)) x =
    Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc (-1) 1) x) (sin (↑x : ℝ)) ⋯

Tactic:
rfl

Premises used: Real.sin, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : √2 / 2 / (√2 / 2) = 1
⊢ tan (π / 4) = 1

Tactic:
rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four]

Premises used: Real.cos_pi_div_four, Real.tan_eq_sin_div_cos, Real.sin_pi_div_four
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ √2 / 2 > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ √2 / 2 > 0

Tactic:
have h : √2 / 2 > 0 := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : √2 / 2 > 0
⊢ √2 / 2 / (√2 / 2) = 1

Tactic:
div_self (ne_of_gt h)

Premises used: ne_of_gt, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : √2 / 2 > 0
⊢ √2 / 2 / (√2 / 2) = 1

Tactic:
exact div_self (ne_of_gt h)

Premises used: ne_of_gt, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ tan (π / 2) = 0

Tactic:
simp [tan_eq_sin_div_cos]

Premises used: Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : 1 / 2 / (√3 / 2) = 1 / √3
⊢ tan (π / 6) = 1 / √3

Tactic:
rw [tan_eq_sin_div_cos, sin_pi_div_six, cos_pi_div_six]

Premises used: Real.cos_pi_div_six, Real.sin_pi_div_six, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 1 / 2 / (√3 / 2) = 1 / √3

Tactic:
ring