awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : π / 5 < -(π / 2) → 5 / 5 = 1
⊢ -(π / 2) ≤ π / 5
have linarith₁ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 2 5 = 10
Tactic: linarith [pi_pos.le]
-- 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 : π / 5 < -(π / 2) → 5 / 5 = 1
linarith₁ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 2 5 = 10
⊢ -(π / 2) ≤ π / 5
have linarith₂ : π / 5 < -(π / 2) → 2 / 2 = 1
Tactic: linarith [pi_pos.le]
-- 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 : π / 5 < -(π / 2) → 5 / 5 = 1
linarith₁ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : π / 5 < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ π / 5
have linarith₃ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 5 2 = 10
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₄ : π / 5 < -(π / 2) → GT.gt (α := ℝ) 10 0
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₅ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₆ : π / 5 < -(π / 2) → 8 / 8 = 1
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₇ : π / 5 < -(π / 2) → HMul.hMul (α := ℝ) 1 8 = 8
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₈ : π / 5 < -(π / 2) → GT.gt (α := ℝ) 8 0
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₉ : π / 5 < -(π / 2) → 2 * π - -(5 * π) + 7 * (0 - π) = 0
Tactic: linarith [pi_pos.le]
-- 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 : π / 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
⊢ -(π / 2) ≤ π / 5
have linarith₁₀ : π / 5 < -(π / 2) → GT.gt (α := ℝ) 7 0
Tactic: linarith [pi_pos.le]
-- 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 ≤ π / 2
have linarith : π / 2 < π / 5 → 2 / 2 = 1
Tactic: linarith [pi_pos.le]
-- 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 < π / 5 → 2 / 2 = 1
⊢ π / 5 ≤ π / 2
have linarith₁ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 5 2 = 10
Tactic: linarith [pi_pos.le]
-- 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 < π / 5 → 2 / 2 = 1
linarith₁ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 5 2 = 10
⊢ π / 5 ≤ π / 2
have linarith₂ : π / 2 < π / 5 → 5 / 5 = 1
Tactic: linarith [pi_pos.le]
-- 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 < π / 5 → 2 / 2 = 1
linarith₁ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 5 2 = 10
linarith₂ : π / 2 < π / 5 → 5 / 5 = 1
⊢ π / 5 ≤ π / 2
have linarith₃ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 2 5 = 10
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₄ : π / 2 < π / 5 → GT.gt (α := ℝ) 10 0
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₅ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₆ : π / 2 < π / 5 → 8 / 8 = 1
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₇ : π / 2 < π / 5 → HMul.hMul (α := ℝ) 1 8 = 8
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₈ : π / 2 < π / 5 → GT.gt (α := ℝ) 8 0
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₉ : π / 2 < π / 5 → 5 * π - 2 * π + 3 * (0 - π) = 0
Tactic: linarith [pi_pos.le]
-- 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 < π / 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
⊢ π / 5 ≤ π / 2
have linarith₁₀ : π / 2 < π / 5 → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos.le]
-- 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 inr : ¬0 ≤ c
Tactic: absurd (show 0 ≤ c from cos_nonneg_of_mem_Icc <| by constructor <;> linarith [pi_pos.le])
-- 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
⊢ ¬0 ≤ c
have inr : (- -2 - 2 * √5) / HMul.hMul (α := ℝ) 2 4 < 0
Tactic: rw [not_le, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ tan (π / 4) = 1
have rw : √2 / 2 / (√2 / 2) = 1
Tactic: rw [tan_eq_sin_div_cos, cos_pi_div_four, sin_pi_div_four]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
⊢ √2 / 2 / (√2 / 2) = 1
have h : √2 / 2 > 0
Tactic: have h : √2 / 2 > 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ tan (π / 6) = 1 / √3
have rw : 1 / 2 / (√3 / 2) = 1 / √3
Tactic: rw [tan_eq_sin_div_cos, sin_pi_div_six, cos_pi_div_six]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ tan (π / 3) = √3
have rw : √3 / 2 / (1 / 2) = √3
Tactic: rw [tan_eq_sin_div_cos, sin_pi_div_three, cos_pi_div_three]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < tan x
have rw : 0 < sin x / cos x
Tactic: rw [tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ x < π
have linarith : π ≤ x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : π ≤ x → 2 / 2 = 1
⊢ x < π
have linarith₁ : π ≤ x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : π ≤ x → 2 / 2 = 1
linarith₁ : π ≤ x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ x < π
have linarith₂ : π ≤ x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : π ≤ x → 2 / 2 = 1
linarith₁ : π ≤ x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π ≤ x → GT.gt (α := ℝ) 2 0
⊢ x < π
have linarith₃ : π ≤ x → 0 - x + (2 * x - 1 * π) + (π - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ -(π / 2) < x
have linarith : x ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : x ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < x
have linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < x
have linarith₂ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < x
have linarith₆ : x ≤ -(π / 2) → 4 * (0 - x) + (2 * x - 1 * π) + (2 * x - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π / 2
linarith : x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : x ≤ -(π / 2) → 4 * (0 - x) + (2 * x - 1 * π) + (2 * x - -(1 * π)) = 0
⊢ -(π / 2) < x
have linarith₇ : x ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ 0 < -x
have linarith : -x ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
linarith : -x ≤ 0 → 2 / 2 = 1
⊢ 0 < -x
have linarith₁ : -x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
linarith : -x ≤ 0 → 2 / 2 = 1
linarith₁ : -x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < -x
have linarith₂ : -x ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
linarith : -x ≤ 0 → 2 / 2 = 1
linarith₁ : -x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -x ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < -x
have linarith₃ : -x ≤ 0 → x - 0 + (-x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
⊢ -x < π / 2
have linarith : π / 2 ≤ -x → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
linarith : π / 2 ≤ -x → 2 / 2 = 1
⊢ -x < π / 2
have linarith₁ : π / 2 ≤ -x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
linarith : π / 2 ≤ -x → 2 / 2 = 1
linarith₁ : π / 2 ≤ -x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -x < π / 2
have linarith₂ : π / 2 ≤ -x → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x < 0
hpx : -(π / 2) < x
linarith : π / 2 ≤ -x → 2 / 2 = 1
linarith₁ : π / 2 ≤ -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ -x → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ -x → 2 / 2 = 1
linarith₄ : π / 2 ≤ -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 ≤ -x → GT.gt (α := ℝ) 2 0
⊢ -x < π / 2
have linarith₆ : π / 2 ≤ -x → -(1 * π) - 2 * x + (1 * π - -(2 * x)) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ 0 ≤ -x
have linarith : -x < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
linarith : -x < 0 → 2 / 2 = 1
⊢ 0 ≤ -x
have linarith₁ : -x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
linarith : -x < 0 → 2 / 2 = 1
linarith₁ : -x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ -x
have linarith₂ : -x < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
linarith : -x < 0 → 2 / 2 = 1
linarith₁ : -x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -x < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ -x
have linarith₃ : -x < 0 → x - 0 + (-x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
⊢ -x ≤ π / 2
have linarith : π / 2 < -x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
linarith : π / 2 < -x → 2 / 2 = 1
⊢ -x ≤ π / 2
have linarith₁ : π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
linarith : π / 2 < -x → 2 / 2 = 1
linarith₁ : π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -x ≤ π / 2
have linarith₂ : π / 2 < -x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx0 : x ≤ 0
hpx : -(π / 2) ≤ x
linarith : π / 2 < -x → 2 / 2 = 1
linarith₁ : π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < -x → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 < -x → 2 / 2 = 1
linarith₄ : π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 < -x → GT.gt (α := ℝ) 2 0
⊢ -x ≤ π / 2
have linarith₆ : π / 2 < -x → -(1 * π) - 2 * x + (1 * π - -(2 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ tan x < tan y
have rw : 0 < sin (y - x)
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos,
    div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy), mul_comm, ← sub_pos, ← sin_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
⊢ y - x < π
have linarith : π ≤ y - x → 2 / 2 = 1
Tactic: linarith [hx.1, hy.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
linarith : π ≤ y - x → 2 / 2 = 1
⊢ y - x < π
have linarith₁ : π ≤ y - x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hx.1, hy.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
linarith : π ≤ y - x → 2 / 2 = 1
linarith₁ : π ≤ y - x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ y - x < π
have linarith₂ : π ≤ y - x → GT.gt (α := ℝ) 2 0
Tactic: linarith [hx.1, hy.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
hlt : x < y
linarith : π ≤ y - x → 2 / 2 = 1
linarith₁ : π ≤ y - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π ≤ y - x → GT.gt (α := ℝ) 2 0
linarith₃ : π ≤ y - x → 2 / 2 = 1
linarith₄ : π ≤ y - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π ≤ y - x → GT.gt (α := ℝ) 2 0
⊢ y - x < π
have linarith₆ : π ≤ y - x → 2 * (π - (y - x)) + (-(1 * π) - 2 * x) + (2 * y - 1 * π) = 0
Tactic: linarith [hx.1, hy.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) < x
have linarith : x ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
linarith : x ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < x
have linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith