awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
have this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
Tactic: have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
    apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
have refine_1 : Real.cos b ≤ Real.cos |z.im|
Tactic: refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
refine_1 : Real.cos b ≤ Real.cos |z.im|
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
have refine_2 : 0 ≤ Real.cos b
Tactic: refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos b
have refine_2 : -(π / 2) ≤ b
Tactic: refine Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Function.Periodic sinh (2 * (↑π : ℂ) * I)
have h : 2 * (↑π : ℂ) * I = 2 * ((↑π : ℂ) * I)
Tactic: convert! sinh_antiperiodic.periodic_two_mul using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Function.Periodic cosh (2 * (↑π : ℂ) * I)
have h : 2 * (↑π : ℂ) * I = 2 * ((↑π : ℂ) * I)
Tactic: convert! cosh_antiperiodic.periodic_two_mul using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
⊢ sin x < x
have inl : ∀ (h' : 1 < x), sin x < x
Tactic: rcases lt_or_ge 1 x with h' | h'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
inl : ∀ (h' : 1 < x), sin x < x
⊢ sin x < x
have inr : ∀ (h' : x ≤ 1), sin x < x
Tactic: rcases lt_or_ge 1 x with h' | h'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < 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
⊢ sin x < x
have this : sin x - (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ HPow.hPow (β := ℕ) |x| 4 * (5 / 96)
Tactic: have := 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 : sin x - (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ HPow.hPow (β := ℕ) |x| 4 * (5 / 96)
⊢ sin x < x
have this₁ : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
Tactic: rw [sub_le_iff_le_add', 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 : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ sin x < x
have inr : x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96) < x
Tactic: apply this.trans_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96) < x
have inr : HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 6⁻¹
Tactic: rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 6⁻¹
have inr : 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 : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3
have inr : 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 (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ sin x ≤ x
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), sin 0 ≤ 0
Tactic: obtain rfl | hx := hx.eq_or_lt
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), sin 0 ≤ 0
⊢ sin x ≤ x
have inr : ∀ (hx : 0 < x), sin x ≤ x
Tactic: obtain rfl | hx := hx.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ 2 / π * x < sin x
have rw : (π / 2)⁻¹ * x < sin x
Tactic: rw [← inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < 1
have rwa : x / (π / 2) < 1
Tactic: rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ 2 / π * x ≤ sin x
have rw : (π / 2)⁻¹ * x ≤ sin x
Tactic: rw [← inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1
have rwa : x / (π / 2) ≤ 1
Tactic: rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : |x| ≤ π / 2
⊢ 2 / π * |x| ≤ |sin x|
have wlog : ∀ (this : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|) (hx₀ : ¬0 ≤ x), 2 / π * |x| ≤ |sin x|
Tactic: wlog hx₀ : 0 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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|
⊢ 2 / π * |x| ≤ |sin x|
have wlog₁ : ∀ {x : ℝ} (hx : |x| ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * |x| ≤ |sin x|
Tactic: wlog hx₀ : 0 ≤ x
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : |x| ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|
have rw : ∀ (hx : x ≤ π / 2) (hx₀ : 0 ≤ x), 2 / π * x ≤ |sin x|
Tactic: rw [abs_of_nonneg hx₀] at hx ⊢
Cleared hypotheses: hx, hx₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
have 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
Tactic: wlog! hx₀ : 0 < x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
have wlog!₁ : ∀ {x : ℝ} (hx : x ≠ 0) (hx₀ : 0 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
Tactic: wlog! hx₀ : 0 < x
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
have rcases : ∀ (hxπ : x ≤ 1), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
Tactic: rcases le_or_gt x 1 with hxπ | hxπ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
rcases : ∀ (hxπ : x ≤ 1), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
have rcases₁ : ∀ (hxπ : 1 < x), HPow.hPow (β := ℕ) (sin x) 2 < HPow.hPow (β := ℕ) x 2
Tactic: rcases le_or_gt x 1 with hxπ | hxπ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ x ≤ π
have linarith : π < x → -1 + (x - 1) + (π - x) + (2 - π) = 0
Tactic: linarith [two_le_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2
have rcases : HPow.hPow (β := ℕ) (sin 0) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 0 2
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
rcases : HPow.hPow (β := ℕ) (sin 0) 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 0 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2
have rcases₁ : ∀ (hx : x ≠ 0), HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) x 2
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
hx : x ≠ 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have this : 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))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x : ℝ
hx : x ≠ 0
this : 1 / 2 - cos (2 * (x / 2)) / 2 < HPow.hPow (β := ℕ) (x / 2) 2
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have this₁ : 1 / 2 + cos x * (-1 / 2) < HPow.hPow (β := ℕ) x 2 * (1 / 4)
Tactic: ring_nf at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : x ≠ 0
this : 1 / 2 + cos x * (-1 / 2) < HPow.hPow (β := ℕ) x 2 * (1 / 4)
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₁ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₂ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₃ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₅ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₈ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₁₀ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have linarith₁₃ : cos x ≤ 1 - HPow.hPow (β := ℕ) x 2 / 2 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 < cos x
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x
have rcases : 1 - HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2 ≤ cos 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
rcases : 1 - HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2 ≤ cos 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x
have rcases₁ : ∀ (hx : x ≠ 0), 1 - HPow.hPow (β := ℕ) x 2 / 2 ≤ cos x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 0 ≤ -x
have linarith : -x < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
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 : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
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.Bounds (goal)
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
⊢ 0 ≤ -x
have linarith₃ : -x < 0 → x - 0 + (-x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ -x ≤ π / 2
have linarith : π / 2 < -x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
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.Bounds (goal)
Goal:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
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.Bounds (goal)
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
⊢ -x ≤ π / 2
have linarith₆ : π / 2 < -x → -(1 * π) - 2 * x + (1 * π - -(2 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
hx : |x| ≤ π
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
have 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
Tactic: wlog hx₀ : 0 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
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
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
have wlog₁ : ∀ {x : ℝ} (hx : |x| ≤ π) (hx₀ : 0 ≤ x), cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
Tactic: wlog hx₀ : 0 ≤ x
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x_1 x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
have hx₁ : x ≤ π
Tactic: rw [abs_of_nonneg hx₀] at hx
Cleared hypotheses: hx, hx₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / 2 ≤ π / 2
have linarith : π / 2 < x / 2 → 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
linarith : π / 2 < x / 2 → 2 / 2 = 1
⊢ x / 2 ≤ π / 2
have linarith₁ : π / 2 < x / 2 → 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
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
⊢ x / 2 ≤ π / 2
have linarith₄ : π / 2 < x / 2 → 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
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
⊢ x / 2 ≤ π / 2
have linarith₅ : π / 2 < x / 2 → x - π + (1 * π - 1 * x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
have this : x / π ≤ sin (x / 2)
Tactic: have : x / π ≤ sin (x / 2) := by simpa using mul_le_sin (x := x / 2) (by positivity) (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (hypothesis)
Goal:
x_1 x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
have this₁ : 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 _)
-- 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 ≤ 1 / 2 - cos (2 * (x / 2)) / 2
⊢ cos x ≤ 1 - 2 / HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) x 2
have 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
Tactic: ring_nf at this ⊢
Cleared hypotheses: this