awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ sin x ≤ x

Tactic:
(sin_lt hx).le

Premises used: Real.sin_lt, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 0 < x
⊢ sin x ≤ x

Tactic:
exact (sin_lt hx).le

Premises used: Real.sin_lt, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x < 0
⊢ x < sin x

Tactic:
simpa using sin_lt <| neg_pos.2 hx

Premises used: Iff.mpr, Real.sin_lt, neg_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≤ 0
⊢ x ≤ sin x

Tactic:
simpa using sin_le <| neg_nonneg.2 hx

Premises used: Iff.mpr, neg_nonneg, Real.sin_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)

Tactic:
simpa [mul_comm x] using
    strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩
      pi_div_two_pos.ne (sub_pos.2 hx') hx

Premises used: Iff.mpr, sub_pos, le_rfl, Real.pi_div_two_pos, Real.pi_pos, LT.lt.le, And.right, half_le_self, And.intro, mul_comm, strictConcaveOn_sin_Icc, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ 1
⊢ x ≤ sin (π / 2 * x)

Tactic:
simpa [mul_comm x] using
    strictConcaveOn_sin_Icc.concaveOn.2 ⟨le_rfl, pi_pos.le⟩
      ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩ (sub_nonneg.2 hx') hx

Premises used: Iff.mpr, le_rfl, Real.pi_div_two_pos, Real.pi_pos, LT.lt.le, And.right, half_le_self, And.intro, mul_comm, strictConcaveOn_sin_Icc, StrictConcaveOn.concaveOn, sub_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 < x
hx' : x < π / 2
rw : (π / 2)⁻¹ * x < sin x
⊢ 2 / π * x < sin x

Tactic:
rw [← inv_div]

Premises used: inv_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 < x
hx' : x < π / 2
rwa : x / (π / 2) < 1
rwa₁ rwa₂ rwa₃ rwa₄ : x < π / 2
⊢ (π / 2)⁻¹ * x < 1

Tactic:
rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos]

Premises used: Real.pi_div_two_pos, div_lt_one, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x

Tactic:
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using @lt_sin_mul ((π / 2)⁻¹ * x)
    (mul_pos (inv_pos.2 pi_div_two_pos) hx) (by rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos])

Premises used: Iff.mpr, mul_inv_cancel_left₀, Real.pi_div_two_pos, inv_pos, LT.lt.ne', mul_pos, Real.lt_sin_mul, inv_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
rw : (π / 2)⁻¹ * x ≤ sin x
⊢ 2 / π * x ≤ sin x

Tactic:
rw [← inv_div]

Premises used: inv_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
rwa : x / (π / 2) ≤ 1
rwa₁ rwa₂ rwa₃ rwa₄ : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1

Tactic:
rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos]

Premises used: Real.pi_div_two_pos, div_le_one, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x

Tactic:
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using @le_sin_mul ((π / 2)⁻¹ * x)
    (mul_nonneg (inv_nonneg.2 pi_div_two_pos.le) hx)
    (by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos])

Premises used: Iff.mpr, mul_nonneg, mul_inv_cancel_left₀, Real.pi_div_two_pos, LT.lt.le, LT.lt.ne', inv_nonneg, inv_div, Real.le_sin_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : -(π / 2) ≤ x
hx₀ : x ≤ 0
⊢ sin x ≤ 2 / π * x

Tactic:
simpa using mul_le_sin (neg_nonneg.2 hx₀) (neg_le.2 hx)

Premises used: Iff.mpr, neg_le, Real.mul_le_sin, neg_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π / 2
wlog :
  ∀ (this : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|) (hx₀ : ¬0 ≤ x), 2 / π * |x| ≤ |sin x|
wlog₁ : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
wlog hx₀ : 0 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
rwa rwa₁ rwa₂ rwa₃ : |x| ≤ π / 2
⊢ |(-x)| ≤ π / 2

Tactic:
rwa [abs_neg]

Premises used: abs_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_ge hx₀

Premises used: Iff.mpr, le_of_not_ge, neg_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
case inr => simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_ge hx₀

Premises used: Iff.mpr, le_of_not_ge, neg_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : |x| ≤ π / 2
hx₀ : 0 ≤ x
rw : ∀ (hx : x ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * x ≤ |sin x|
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
rw [abs_of_nonneg hx₀] at hx ⊢

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * x ≤ |sin x|

Tactic:
(mul_le_sin hx₀ hx).trans (le_abs_self _)

Premises used: le_abs_self, Real.mul_le_sin, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * x ≤ |sin x|

Tactic:
exact (mul_le_sin hx₀ hx).trans (le_abs_self _)

Premises used: le_abs_self, Real.mul_le_sin, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
wlog! :
  ∀ (this : ∀ {x : ℝ} (hx : x ≠ 0) (hx₀ : 0 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2) (hx₀ : x ≤ 0),
    HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
wlog!₁ : ∀ {x : ℝ} (hx : x ≠ 0) (hx₀ : 0 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
wlog! hx₀ : 0 < x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
this : ∀ {x : ℝ} (hx : x ≠ 0) (hx₀ : 0 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
hx₀ : x ≤ 0
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
simpa using this (neg_ne_zero.2 hx) <| neg_pos_of_neg <| hx.lt_of_le hx₀

Premises used: Iff.mpr, neg_pos_of_neg, neg_ne_zero, Ne.lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
this : ∀ {x : ℝ} (hx : x ≠ 0) (hx₀ : 0 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
hx₀ : x ≤ 0
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
case inr =>
    simpa using this (neg_ne_zero.2 hx) <| neg_pos_of_neg <| hx.lt_of_le hx₀

Premises used: Iff.mpr, neg_pos_of_neg, neg_ne_zero, Ne.lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
rcases : ∀ (hxπ : x ≤ 1), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
rcases₁ : ∀ (hxπ : 1 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
rcases le_or_gt x 1 with hxπ | hxπ

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
linarith : π < x → -1 + (x - 1) + (π - x) + (2 - π) = 0
⊢ x ≤ π

Tactic:
linarith [two_le_pi]

Premises used: Real.two_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
exact pow_lt_pow_left₀ (sin_lt hx₀)
      (sin_nonneg_of_nonneg_of_le_pi hx₀.le (by linarith [two_le_pi])) (by simp)

Premises used: Real.sin_lt, Real.sin_nonneg_of_nonneg_of_le_pi, LT.lt.le, pow_lt_pow_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
case inl =>
    exact pow_lt_pow_left₀ (sin_lt hx₀)
      (sin_nonneg_of_nonneg_of_le_pi hx₀.le (by linarith [two_le_pi])) (by simp)

Premises used: Real.sin_lt, Real.sin_nonneg_of_nonneg_of_le_pi, LT.lt.le, pow_lt_pow_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
rwa rwa₁ rwa₂ rwa₃ : 1 < x
⊢ 1 < HPow.hPow (β := ℕ) x 2

Tactic:
rwa [one_lt_sq_iff₀ hx₀.le]

Premises used: one_lt_sq_iff₀, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
exact (sin_sq_le_one _).trans_lt (by rwa [one_lt_sq_iff₀ hx₀.le])

Premises used: Real.sin_sq_le_one, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2

Tactic:
case inr =>
    exact (sin_sq_le_one _).trans_lt (by rwa [one_lt_sq_iff₀ hx₀.le])

Premises used: Real.sin_sq_le_one, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rcases : HPow.hPow (β := ℕ) (sin 0) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 0 2
rcases₁ : ∀ (hx : x ≠ 0), HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
⊢ HPow.hPow (β := ℕ) (sin 0) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
⊢ HPow.hPow (β := ℕ) (sin 0) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 0 2

Tactic:
case inl => simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
(sin_sq_lt_sq hx).le

Premises used: LT.lt.le, Real.sin_sq_lt_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
exact (sin_sq_lt_sq hx).le

Premises used: LT.lt.le, Real.sin_sq_lt_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
case inr => exact (sin_sq_lt_sq hx).le

Premises used: LT.lt.le, Real.sin_sq_lt_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ |sin x| < |x|

Tactic:
sq_lt_sq.1 (sin_sq_lt_sq hx)

Premises used: sq_lt_sq, Iff.mp, Real.sin_sq_lt_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ |sin x| ≤ |x|

Tactic:
sq_le_sq.1 sin_sq_le_sq

Premises used: sq_le_sq, Real.sin_sq_le_sq, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ x / 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ 1 / 2 - cos (2 * (x / 2)) / 2 < HPow.hPow (β := ℕ) (x / 2) 2

Tactic:
have := (sin_sq_lt_sq (by positivity)).trans_eq' (sin_sq_eq_half_sub (x / 2))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
this : 1 / 2 - cos (2 * (x / 2)) / 2 < HPow.hPow (β := ℕ) (x / 2) 2
⊢ 1 / 2 + cos x * (-1 / 2) < HPow.hPow (β := ℕ) x 2 * (1 / 4)

Tactic:
ring_nf at this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
this : 1 / 2 + cos x * (-1 / 2) < HPow.hPow (β := ℕ) x 2 * (1 / 4)
linarith : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 2 / 2 = 1
linarith₂ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → GT.gt (α := ℝ) 2 0
linarith₄ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 2 / 2 = 1
linarith₅ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₆ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 2 / 2 = 1
linarith₇ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₈ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₉ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁₀ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 4 / 4 = 1
linarith₁₁ linarith₁₂ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₃ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → GT.gt (α := ℝ) 4 0
linarith₁₄ :
  cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 →
    HMul.hMul (α := ℝ) 2 1 + 1 * cos x * -HMul.hMul (α := ℝ) 2 1 -
          1 * HPow.hPow (β := ℕ) (1 * x) 2 * HMul.hMul (α := ℝ) 1 1 +
        (2 * cos x - (HMul.hMul (α := ℝ) 2 1 - 1 * HPow.hPow (β := ℕ) (1 * x) 2)) =
      0
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rcases : 1 - HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2 ≤ cos 0
rcases₁ : ∀ (hx : x ≠ 0), 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
⊢ 1 - HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2 ≤ cos 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
⊢ 1 - HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2 ≤ cos 0

Tactic:
case inl => simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x

Tactic:
(one_sub_sq_div_two_lt_cos hx).le

Premises used: LT.lt.le, Real.one_sub_sq_div_two_lt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x

Tactic:
exact (one_sub_sq_div_two_lt_cos hx).le

Premises used: LT.lt.le, Real.one_sub_sq_div_two_lt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : x ≠ 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x

Tactic:
case inr => exact (one_sub_sq_div_two_lt_cos hx).le

Premises used: LT.lt.le, Real.one_sub_sq_div_two_lt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ 0 ≤ π / 2 - x

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ π / 2 - x ≤ π / 2

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ 1 - 2 / π * x ≤ cos x

Tactic:
simpa [sin_pi_div_two_sub, mul_sub, div_mul_div_comm, mul_comm π, pi_pos.ne']
    using mul_le_sin (x := π / 2 - x) (by simpa) (by simpa)

Premises used: Real.pi, mul_sub, div_mul_div_comm, Real.mul_le_sin, Real.sin_pi_div_two_sub, Real.pi_pos, LT.lt.ne', mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
linarith : -x < 0 → 2 / 2 = 1
linarith₁ : -x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -x < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : -x < 0 → x - 0 + (-x - 0) = 0
⊢ 0 ≤ -x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
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
linarith₆ : π / 2 < -x → -(1 * π) - 2 * x + (1 * π - -(2 * x)) = 0
⊢ -x ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 1 + 2 / π * x ≤ cos x

Tactic:
simpa using one_sub_mul_le_cos (x := -x) (by linarith) (by linarith)

Premises used: Real.one_sub_mul_le_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π
wlog :
  ∀ (this : ∀ {x : ℝ} (hx : |x| ≤ π) (hx₀ : 0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2)
    (hx₀ : ¬0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
wlog₁ : ∀ {x : ℝ} (hx : |x| ≤ π) (hx₀ : 0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2

Tactic:
wlog hx₀ : 0 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ} (hx : |x| ≤ π) (hx₀ : 0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
hx₀ : ¬0 ≤ x
rwa rwa₁ rwa₂ rwa₃ : |x| ≤ π
⊢ |(-x)| ≤ π

Tactic:
rwa [abs_neg]

Premises used: abs_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ} (hx : |x| ≤ π) (hx₀ : 0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
hx₀ : ¬0 ≤ x
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2

Tactic:
simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_ge hx₀

Premises used: Iff.mpr, le_of_not_ge, neg_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ} (hx : |x| ≤ π) (hx₀ : 0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
hx₀ : ¬0 ≤ x
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2

Tactic:
case inr => simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_ge hx₀

Premises used: Iff.mpr, le_of_not_ge, neg_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
⊢ x ≤ π

Tactic:
rw [abs_of_nonneg hx₀] at hx

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
hx₁ : x ≤ π
⊢ 0 ≤ x

Tactic:
rw [abs_of_nonneg hx₀] at hx

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ 0 ≤ x / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
linarith : π / 2 < x / 2 → 2 / 2 = 1
linarith₁ : π / 2 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < x / 2 → 2 / 2 = 1
linarith₃ : π / 2 < x / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 < x / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π / 2 < x / 2 → x - π + (1 * π - 1 * x) = 0
⊢ x / 2 ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / π ≤ sin (x / 2)

Tactic:
simpa using mul_le_sin (x := x / 2) (by positivity) (by linarith)

Premises used: Real.mul_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / π ≤ sin (x / 2)

Tactic:
have : x / π ≤ sin (x / 2) := by simpa using mul_le_sin (x := x / 2) (by positivity) (by linarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ 0 ≤ x / π

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ HPow.hPow (β := ℕ) (x / π) 2 ≤ 1 / 2 - cos (2 * (x / 2)) / 2

Tactic:
have := (pow_le_pow_left₀ (by positivity) this 2).trans_eq (sin_sq_eq_half_sub _)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this_1 : x / π ≤ sin (x / 2)
this : HPow.hPow (β := ℕ) (x / π) 2 ≤ 1 / 2 - cos (2 * (x / 2)) / 2
ring_nf :
  ∀ (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
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2

Tactic:
ring_nf at this ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
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
⊢ cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 * HPow.hPow (β := ℕ) π⁻¹ 2 * 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ -(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])
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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)
⊢ -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ sin x

Tactic:
rw [le_sub_iff_add_le, hx] at this

Premises used: le_sub_iff_add_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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

Tactic:
lt_of_lt_of_le ?_ this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
refine : x - HPow.hPow (β := ℕ) x 3 / 4 < -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6)
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < sin x

Tactic:
refine lt_of_lt_of_le ?_ this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ HPow.hPow (β := ℕ) x 3 / 4 - HPow.hPow (β := ℕ) x 3 / 6 = HPow.hPow (β := ℕ) x 3 * 12⁻¹

Tactic:
norm_num [div_eq_mul_inv, ← mul_sub]

Premises used: mul_sub, div_eq_mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ 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]