awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
linarith linarith₁ :
  1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith₂ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
linarith linarith₁ :
  1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ linarith₃ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith₅ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
linarith linarith₁ :
  1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ linarith₃ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₅ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 2
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith₆ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
linarith linarith₁ :
  1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ linarith₃ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₅ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 2
linarith₆ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith₇ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
linarith linarith₁ :
  1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ linarith₃ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₅ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 2
linarith₆ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 / 2 = 1
linarith₈ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 / 2 = 1
linarith₁₀ linarith₁₁ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith₁₂ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 ≤ 1 / 2 + cos x * (-1 / 2)
linarith linarith₁ :
  1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₂ linarith₃ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₅ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 2
linarith₆ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 / 2 = 1
linarith₈ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → 2 / 2 = 1
linarith₁₀ linarith₁₁ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x → GT.gt (α := ℝ) 2 0
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2
have linarith₁₃ : 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2 < cos x →
  1 * HPow.hPow (β := ℕ) (1 * x) 2 * (2 * HPow.hPow (β := ℕ) (1 * π⁻¹) 2) -
        (HMul.hMul (α := ℝ) 1 1 + 1 * cos x * -HMul.hMul (α := ℝ) 1 1) +
      (HMul.hMul (α := ℝ) 1 1 -
          1 * HPow.hPow (β := ℕ) (1 * x) 2 * (1 * HPow.hPow (β := ℕ) (1 * π⁻¹) 2) * HMul.hMul (α := ℝ) 1 2 -
        1 * cos x) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < sin x
have hx : |x| = x
Tactic: have hx : |x| = x := abs_of_nonneg h.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < sin x
have this : -(HPow.hPow (β := ℕ) |x| 4 * (5 / 96)) ≤ sin x - (x - HPow.hPow (β := ℕ) x 3 / 6)
Tactic: have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(HPow.hPow (β := ℕ) |x| 4 * (5 / 96)) ≤ sin x - (x - HPow.hPow (β := ℕ) x 3 / 6)
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < sin x
have this₁ : -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x
Tactic: rw [le_sub_iff_add_le, hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < sin x
have refine : x - HPow.hPow (β := ℕ) x 3 / 4 < -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6)
Tactic: refine lt_of_lt_of_le ?_ this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6)
have this₁ : HPow.hPow (β := ℕ) x 3 / 4 - HPow.hPow (β := ℕ) x 3 / 6 = HPow.hPow (β := ℕ) x 3 * 12⁻¹
Tactic: have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by norm_num [div_eq_mul_inv, ← mul_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this_1 : -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x
this : HPow.hPow (β := ℕ) x 3 / 4 - HPow.hPow (β := ℕ) x 3 / 6 = HPow.hPow (β := ℕ) x 3 * 12⁻¹
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6)
have rw : HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 12⁻¹
Tactic: rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this_1 : -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x
this : HPow.hPow (β := ℕ) x 3 / 4 - HPow.hPow (β := ℕ) x 3 / 6 = HPow.hPow (β := ℕ) x 3 * 12⁻¹
⊢ HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 12⁻¹
have refine : HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3
Tactic: refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this_1 : -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x
this : HPow.hPow (β := ℕ) x 3 / 4 - HPow.hPow (β := ℕ) x 3 / 6 = HPow.hPow (β := ℕ) x 3 * 12⁻¹
⊢ HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3
have apply : LE.le (α := ℕ) 3 4
Tactic: apply pow_le_pow_of_le_one h.le h'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
⊢ x < tan x
have intU : interior U = Ioo 0 (π / 2)
Tactic: have intU : interior U = Ioo 0 (π / 2) := interior_Ico
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
⊢ x < tan x
have half_pi_pos : 0 < π / 2
Tactic: have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
⊢ x < tan x
have cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
Tactic: have cos_pos {y : ℝ} (hy : y ∈ U) : 0 < cos y := by
    exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
y : ℝ
hy : y ∈ interior U
⊢ 0 < sin y
have hy₁ : y ∈ Ioo 0 (π / 2)
Tactic: rw [intU] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
⊢ x < tan x
have sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
Tactic: have sin_pos {y : ℝ} (hy : y ∈ interior U) : 0 < sin y := by
    rw [intU] at hy
    exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
⊢ ContinuousOn tan U
have apply : U ⊆ {x : ℝ | cos x ≠ 0}
Tactic: apply ContinuousOn.mono continuousOn_tan
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
⊢ x < tan x
have tan_cts_U : ContinuousOn tan U
Tactic: have tan_cts_U : ContinuousOn tan U := by
    apply ContinuousOn.mono continuousOn_tan
    intro z hz
    simp only [mem_setOf_eq]
    exact (cos_pos hz).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
⊢ x < tan x
have tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
Tactic: have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
⊢ LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)
have this : 0 < cos y
Tactic: have := cos_pos (interior_subset hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)
have simp : 1 < (HPow.hPow (β := ℕ) (cos y) 2)⁻¹
Tactic: simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ HPow.hPow (β := ℕ) (cos y) 2 < 1
have apply : HPow.hPow (β := ℕ) (cos y) 2 ≠ 1
Tactic: apply lt_of_le_of_ne y.cos_sq_le_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ HPow.hPow (β := ℕ) (cos y) 2 ≠ 1
have rw : 1 - HPow.hPow (β := ℕ) (sin y) 2 ≠ 1
Tactic: rw [cos_sq']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 < (HPow.hPow (β := ℕ) (cos y) 2)⁻¹
have bd2 : HPow.hPow (β := ℕ) (cos y) 2 < 1
Tactic: have bd2 : cos y ^ 2 < 1 := by
      apply lt_of_le_of_ne y.cos_sq_le_one
      rw [cos_sq']
      simpa only [Ne, sub_eq_self, sq_eq_zero_iff] using (sin_pos hy).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : HPow.hPow (β := ℕ) (cos y) 2 < 1
⊢ 1 < (HPow.hPow (β := ℕ) (cos y) 2)⁻¹
have ha : LT.lt (α := ℝ) 0 1
Tactic: rwa [lt_inv_comm₀, inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : HPow.hPow (β := ℕ) (cos y) 2 < 1
ha : LT.lt (α := ℝ) 0 1
⊢ 1 < (HPow.hPow (β := ℕ) (cos y) 2)⁻¹
have hb : 0 < HPow.hPow (β := ℕ) (cos y) 2
Tactic: rwa [lt_inv_comm₀, inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
⊢ x < tan x
have deriv_pos : ∀ (y : ℝ) (hy : y ∈ interior U), LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)
Tactic: have deriv_pos (y : ℝ) (hy : y ∈ interior U) : 0 < deriv (fun y' : ℝ => tan y' - y') y := by
    have := cos_pos (interior_subset hy)
    simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
    norm_cast
    have bd2 : cos y ^ 2 < 1 := by
      apply lt_of_le_of_ne y.cos_sq_le_one
      rw [cos_sq']
      simpa only [Ne, sub_eq_self, sq_eq_zero_iff] using (sin_pos hy).ne'
    rwa [lt_inv_comm₀, inv_one]
    · exact zero_lt_one
    simpa only [sq, mul_self_pos] using this.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
deriv_pos : ∀ (y : ℝ) (hy : y ∈ interior U), LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)
⊢ x < tan x
have mono : StrictMonoOn (β := ℝ) (fun (y : ℝ) ↦ tan y - y) (Ico 0 (π / 2))
Tactic: have mono := strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
deriv_pos : ∀ (y : ℝ) (hy : y ∈ interior U), LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)
mono : StrictMonoOn (β := ℝ) (fun (y : ℝ) ↦ tan y - y) (Ico 0 (π / 2))
⊢ x < tan x
have zero_in_U : 0 ∈ U
Tactic: have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ} (hy : y ∈ U), 0 < cos y
sin_pos : ∀ {y : ℝ} (hy : y ∈ interior U), 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (Y := ℝ) (fun (y : ℝ) ↦ tan y - y) U
deriv_pos : ∀ (y : ℝ) (hy : y ∈ interior U), LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)
mono : StrictMonoOn (β := ℝ) (fun (y : ℝ) ↦ tan y - y) (Ico 0 (π / 2))
zero_in_U : 0 ∈ U
⊢ x < tan x
have x_in_U : x ∈ U
Tactic: have x_in_U : x ∈ U := ⟨h1.le, h2⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x
have inl : ∀ (h1 : LE.le (α := ℝ) 0 0) (h2 : 0 < π / 2), 0 ≤ tan 0
Tactic: rcases eq_or_lt_of_le h1 with (rfl | h1')
Cleared hypotheses: x, h1, h2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
inl : ∀ (h1 : LE.le (α := ℝ) 0 0) (h2 : 0 < π / 2), 0 ≤ tan 0
⊢ x ≤ tan x
have inr : ∀ (h1' : 0 < x), x ≤ tan x
Tactic: rcases eq_or_lt_of_le h1 with (rfl | h1')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
have inl : ∀ (h : 0 < x), cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
Tactic: rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
inl : ∀ (h : 0 < x), cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
have inr : x < 0 → cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
Tactic: rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
h : x < 0
⊢ 0 < -x
have linarith : -x ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
h : x < 0
linarith : -x ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ 0 < -x
have linarith₁ : -x ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
h : x < 0
linarith : -x ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
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.Bounds (goal)
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
h : x < 0
linarith : -x ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
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