awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < sin ((y - x) / 2)
have h0x : 0 < (y - x) / 2
Tactic: apply sin_pos_of_pos_of_lt_pi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
h0x : 0 < (y - x) / 2
⊢ 0 < sin ((y - x) / 2)
have hxp : (y - x) / 2 < π
Tactic: apply sin_pos_of_pos_of_lt_pi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < (y - x) / 2
have linarith : (y - x) / 2 ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
linarith : (y - x) / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < (y - x) / 2
have linarith₁ : (y - x) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
linarith : (y - x) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (y - x) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < (y - x) / 2
have linarith₂ : (y - x) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
linarith : (y - x) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (y - x) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (y - x) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (y - x) / 2 ≤ 0 → 2 / 2 = 1
linarith₄ : (y - x) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : (y - x) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₆ : (y - x) / 2 ≤ 0 → 2 / 2 = 1
linarith₇ : (y - x) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : (y - x) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < (y - x) / 2
have linarith₉ : (y - x) / 2 ≤ 0 → x - y + (1 * y - 1 * x - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ (y - x) / 2 < π
have linarith : π ≤ (y - x) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
linarith : π ≤ (y - x) / 2 → 2 / 2 = 1
⊢ (y - x) / 2 < π
have linarith₁ : π ≤ (y - x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
linarith : π ≤ (y - x) / 2 → 2 / 2 = 1
linarith₁ : π ≤ (y - x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (y - x) / 2 < π
have linarith₂ : π ≤ (y - x) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
linarith : π ≤ (y - x) / 2 → 2 / 2 = 1
linarith₁ : π ≤ (y - x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π ≤ (y - x) / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π ≤ (y - x) / 2 → 2 / 2 = 1
linarith₄ : π ≤ (y - x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π ≤ (y - x) / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : π ≤ (y - x) / 2 → 2 / 2 = 1
linarith₇ : π ≤ (y - x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π ≤ (y - x) / 2 → GT.gt (α := ℝ) 2 0
⊢ (y - x) / 2 < π
have linarith₉ : π ≤ (y - x) / 2 → -(1 * π) - 2 * x + (2 * y - 1 * π) + (x - y) + (2 * π - (1 * y - 1 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
have this : 0 < sin ((y - x) / 2)
Tactic: have : 0 < sin ((y - x) / 2) := by apply sin_pos_of_pos_of_lt_pi <;> linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < cos ((y + x) / 2)
have refine_1 : -(π / 2) < (y + x) / 2
Tactic: refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
refine_1 : -(π / 2) < (y + x) / 2
⊢ 0 < cos ((y + x) / 2)
have refine_2 : (y + x) / 2 < π / 2
Tactic: refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ -(π / 2) < (y + x) / 2
have linarith : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
linarith : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < (y + x) / 2
have linarith₁ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
linarith : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
linarith₃ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < (y + x) / 2
have linarith₄ : (y + x) / 2 ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
linarith : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
linarith₃ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : (y + x) / 2 ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₅ : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
linarith₆ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : (y + x) / 2 ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₈ : (y + x) / 2 ≤ -(π / 2) → 2 / 2 = 1
linarith₉ : (y + x) / 2 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : (y + x) / 2 ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < (y + x) / 2
have linarith₁₁ : (y + x) / 2 ≤ -(π / 2) → -(1 * π) - 2 * x + (x - y) + (1 * y + 1 * x - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ (y + x) / 2 < π / 2
have linarith : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
linarith : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
⊢ (y + x) / 2 < π / 2
have linarith₁ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
linarith : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
linarith₁ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
linarith₃ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (y + x) / 2 < π / 2
have linarith₄ : π / 2 ≤ (y + x) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
linarith : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
linarith₁ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
linarith₃ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 ≤ (y + x) / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
linarith₆ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π / 2 ≤ (y + x) / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π / 2 ≤ (y + x) / 2 → 2 / 2 = 1
linarith₉ : π / 2 ≤ (y + x) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : π / 2 ≤ (y + x) / 2 → GT.gt (α := ℝ) 2 0
⊢ (y + x) / 2 < π / 2
have linarith₁₁ : π / 2 ≤ (y + x) / 2 → 2 * y - 1 * π + (x - y) + (1 * π - (1 * y + 1 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
have this₁ : 0 < cos ((y + x) / 2)
Tactic: have : 0 < cos ((y + x) / 2) := by refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ cos y < cos x
have rw : sin (π / 2 - y) < sin (π / 2 - x)
Tactic: rw [← sin_pi_div_two_sub, ← sin_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < sin (π / 2 - x)
have hx₂ : -(π / 2) ≤ π / 2 - y
Tactic: apply sin_lt_sin_of_lt_of_le_pi_div_two
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx₂ : -(π / 2) ≤ π / 2 - y
⊢ sin (π / 2 - y) < sin (π / 2 - x)
have hy₃ : π / 2 - x ≤ π / 2
Tactic: apply sin_lt_sin_of_lt_of_le_pi_div_two
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
hx₂ : -(π / 2) ≤ π / 2 - y
hy₃ : π / 2 - x ≤ π / 2
⊢ sin (π / 2 - y) < sin (π / 2 - x)
have hxy₁ : π / 2 - y < π / 2 - x
Tactic: apply sin_lt_sin_of_lt_of_le_pi_div_two
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ -(π / 2) ≤ π / 2 - y
have linarith : π / 2 - y < -(π / 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 ≤ π
hxy : x < y
linarith : π / 2 - y < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ π / 2 - y
have linarith₁ : π / 2 - y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 - y < -(π / 2) → 2 / 2 = 1
linarith₁ : π / 2 - y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 - y < -(π / 2) → 2 / 2 = 1
linarith₃ : π / 2 - y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) ≤ π / 2 - y
have linarith₄ : π / 2 - y < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 - y < -(π / 2) → 2 / 2 = 1
linarith₁ : π / 2 - y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 - y < -(π / 2) → 2 / 2 = 1
linarith₃ : π / 2 - y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 - y < -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) ≤ π / 2 - y
have linarith₅ : π / 2 - y < -(π / 2) → 2 * (y - π) + (1 * π - 2 * y - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ π / 2 - x ≤ π / 2
have linarith : π / 2 < π / 2 - x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 < π / 2 - x → 2 / 2 = 1
⊢ π / 2 - x ≤ π / 2
have linarith₁ : π / 2 < π / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 < π / 2 - x → 2 / 2 = 1
linarith₁ : π / 2 < π / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < π / 2 - x → 2 / 2 = 1
linarith₃ : π / 2 < π / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 - x ≤ π / 2
have linarith₄ : π / 2 < π / 2 - x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 < π / 2 - x → 2 / 2 = 1
linarith₁ : π / 2 < π / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < π / 2 - x → 2 / 2 = 1
linarith₃ : π / 2 < π / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 < π / 2 - x → GT.gt (α := ℝ) 2 0
⊢ π / 2 - x ≤ π / 2
have linarith₅ : π / 2 < π / 2 - x → 2 * (0 - x) + (1 * π - (1 * π - 2 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ π / 2 - y < π / 2 - x
have linarith : π / 2 - x ≤ π / 2 - y → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 - x ≤ π / 2 - y → 2 / 2 = 1
⊢ π / 2 - y < π / 2 - x
have linarith₁ : π / 2 - x ≤ π / 2 - y → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 - x ≤ π / 2 - y → 2 / 2 = 1
linarith₁ : π / 2 - x ≤ π / 2 - y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 - x ≤ π / 2 - y → 2 / 2 = 1
linarith₃ : π / 2 - x ≤ π / 2 - y → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 - y < π / 2 - x
have linarith₄ : π / 2 - x ≤ π / 2 - y → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
linarith : π / 2 - x ≤ π / 2 - y → 2 / 2 = 1
linarith₁ : π / 2 - x ≤ π / 2 - y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 - x ≤ π / 2 - y → 2 / 2 = 1
linarith₃ : π / 2 - x ≤ π / 2 - y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 - x ≤ π / 2 - y → GT.gt (α := ℝ) 2 0
⊢ π / 2 - y < π / 2 - x
have linarith₅ : π / 2 - x ≤ π / 2 - y → 2 * (x - y) + (1 * π - 2 * x - (1 * π - 2 * y)) = 0
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
⊢ π / 2 ≤ π
have linarith : π < π / 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 : π < π / 2 → 2 / 2 = 1
⊢ π / 2 ≤ π
have linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
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 : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 ≤ π
have linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
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 : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < π / 2 → 2 / 2 = 1
linarith₄ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π < π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 ≤ π
have linarith₆ : π < π / 2 → 2 * (0 - x) + (2 * y - 1 * π) + 2 * (x - y) + (2 * π - 1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ (range cos).Infinite
have rw : Set.Infinite (α := ℝ) (Icc (-1) 1)
Tactic: rw [Real.range_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ (range sin).Infinite
have rw : Set.Infinite (α := ℝ) (Icc (-1) 1)
Tactic: rw [Real.range_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < 2
have refine : sqrtTwoAddSeries 0 (n + 1) < √(HPow.hPow (α := ℝ) (β := ℕ) 2 2)
Tactic: refine lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < √(HPow.hPow (α := ℝ) (β := ℕ) 2 2)
have rw : sqrtTwoAddSeries 0 n < HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2
Tactic: rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
rw : sqrtTwoAddSeries 0 n < HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2
⊢ sqrtTwoAddSeries 0 (n + 1) < √(HPow.hPow (α := ℝ) (β := ℕ) 2 2)
have rw₁ : 0 ≤ 2 + sqrtTwoAddSeries 0 n
Tactic: rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
⊢ sqrtTwoAddSeries 0 n < HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2
have refine : 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 - 2
Tactic: refine (sqrtTwoAddSeries_lt_two n).trans_le ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
n : ℕ
⊢ x.sqrtTwoAddSeries (n + 1 + 1) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
have rw : √(2 + x.sqrtTwoAddSeries (n + 1)) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
Tactic: rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
n : ℕ
rw : √(2 + x.sqrtTwoAddSeries (n + 1)) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
⊢ x.sqrtTwoAddSeries (n + 1 + 1) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
have rw₁ : √(2 + (√(2 + x)).sqrtTwoAddSeries n) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
Tactic: rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
n : ℕ
rw : √(2 + x.sqrtTwoAddSeries (n + 1)) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
rw₁ : √(2 + (√(2 + x)).sqrtTwoAddSeries n) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
⊢ x.sqrtTwoAddSeries (n + 1 + 1) = (√(2 + x)).sqrtTwoAddSeries (n + 1)
have rw₂ : √(2 + (√(2 + x)).sqrtTwoAddSeries n) = √(2 + (√(2 + x)).sqrtTwoAddSeries n)
Tactic: rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)
have a : x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℕ
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
Tactic: have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: have C : 0 < π / 2 ^ (n + 1) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have rw : LE.le (α := ℝ) 0 2
Tactic: rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
rw : LE.le (α := ℝ) 0 2
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have hx : 0 ≤ 2 + sqrtTwoAddSeries 0 n
Tactic: rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
rw : LE.le (α := ℝ) 0 2
hx : 0 ≤ 2 + sqrtTwoAddSeries 0 n
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have hc : Ne (α := ℝ) 2 0
Tactic: rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
rw : LE.le (α := ℝ) 0 2
hx : 0 ≤ 2 + sqrtTwoAddSeries 0 n
hc : Ne (α := ℝ) 2 0
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have hl : -π ≤ π / HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
rw : LE.le (α := ℝ) 0 2
hx : 0 ≤ 2 + sqrtTwoAddSeries 0 n
hc : Ne (α := ℝ) 2 0
hl : -π ≤ π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ cos (π / HPow.hPow (α := ℝ) 2 (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
have hr : π / HPow.hPow (α := ℝ) 2 (n + 1) ≤ π
Tactic: rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ LE.le (α := ℝ) 0 2
have linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
linarith : LT.lt (α := ℝ) 2 0 → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 2 0 = 0
⊢ LE.le (α := ℝ) 0 2
have linarith₁ : LT.lt (α := ℝ) 2 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
have linarith : 2 + sqrtTwoAddSeries 0 n < 0 →
  HMul.hMul (α := ℝ) 2 (-1) + (2 + sqrtTwoAddSeries 0 n - 0) + (0 - sqrtTwoAddSeries 0 n) = 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
n : ℕ
A : 1 < HPow.hPow (α := ℝ) 2 (n + 1)
B : π / HPow.hPow (α := ℝ) 2 (n + 1) < π
C : 0 < π / HPow.hPow (α := ℝ) 2 (n + 1)
linarith :
  2 + sqrtTwoAddSeries 0 n < 0 →
    HMul.hMul (α := ℝ) 2 (-1) + (2 + sqrtTwoAddSeries 0 n - 0) + (0 - sqrtTwoAddSeries 0 n) = 0
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
have linarith₁ : 2 + sqrtTwoAddSeries 0 n < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [sqrtTwoAddSeries_nonneg le_rfl n]