awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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⁻¹
rw : HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 12⁻¹
⊢ x - HPow.hPow (β := ℕ) x 3 / 4 < -(HPow.hPow (β := ℕ) x 4 * (5 / 96)) + (x - HPow.hPow (β := ℕ) x 3 / 6)

Tactic:
rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]

Premises used: sub_add, lt_sub_iff_add_lt', add_comm, sub_lt_sub_iff_left, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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⁻¹
⊢ 5 / 96 < 12⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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⁻¹
⊢ 0 ≤ 5 / 96

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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⁻¹
refine : HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3
⊢ HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 12⁻¹

Tactic:
refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)

Premises used: pow_pos, mul_lt_mul', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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⁻¹
apply : LE.le (α := ℕ) 3 4
⊢ HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3

Tactic:
apply pow_le_pow_of_le_one h.le h'

Premises used: LT.lt.le, pow_le_pow_of_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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⁻¹
⊢ LE.le (α := ℕ) 3 4

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt (fun (y : ℝ) ↦ tan y - y) (1 / HPow.hPow (β := ℕ) (cos x) 2 - 1) x

Tactic:
simpa using (hasDerivAt_tan h).add (hasDerivAt_id x).neg

Premises used: HasDerivAt.add, HasDerivAt.neg, Real.hasDerivAt_tan, hasDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
⊢ interior U = Ioo 0 (π / 2)

Tactic:
have intU : interior U = Ioo 0 (π / 2) := interior_Ico
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
⊢ 0 < π / 2

Tactic:
have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
y : ℝ
hy : y ∈ U
⊢ 0 < cos y

Tactic:
cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)

Premises used: Iff.mpr, neg_lt_zero, Real.cos_pos_of_mem_Ioo, Set.Ico_subset_Ioo_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
y : ℝ
hy : y ∈ U
⊢ 0 < cos y

Tactic:
exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)

Premises used: Iff.mpr, neg_lt_zero, Real.cos_pos_of_mem_Ioo, Set.Ico_subset_Ioo_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
⊢ ∀ {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)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ y ∈ Ioo 0 (π / 2)

Tactic:
rw [intU] at hy
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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 ∈ Ioo 0 (π / 2)
⊢ 0 < sin y

Tactic:
sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)

Premises used: Set.Ioo_subset_Ioo_right, Real.pi_pos, LT.lt.le, div_le_self, Real.sin_pos_of_mem_Ioo, one_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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 ∈ Ioo 0 (π / 2)
⊢ 0 < sin y

Tactic:
exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)

Premises used: Set.Ioo_subset_Ioo_right, Real.pi_pos, LT.lt.le, div_le_self, Real.sin_pos_of_mem_Ioo, one_le_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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

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)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
apply : U ⊆ {x : ℝ | cos x ≠ 0}
⊢ ContinuousOn tan U

Tactic:
apply ContinuousOn.mono continuousOn_tan

Premises used: Real.continuousOn_tan, ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
z : ℝ
hz : z ∈ U
⊢ cos z ≠ 0

Tactic:
(cos_pos hz).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
z : ℝ
hz : z ∈ U
⊢ cos z ≠ 0

Tactic:
exact (cos_pos hz).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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

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'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ 0 < cos y

Tactic:
have := cos_pos (interior_subset hy)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
simp : 1 < (HPow.hPow (β := ℕ) (cos y) 2)⁻¹
⊢ LT.lt (α := ℝ) 0 (deriv (fun (y' : ℝ) ↦ tan y' - y') y)

Tactic:
simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]

Premises used: sub_pos, Real.deriv_tan_sub_id, LT.lt.ne', one_div, gt_iff_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
apply : HPow.hPow (β := ℕ) (cos y) 2 ≠ 1
⊢ HPow.hPow (β := ℕ) (cos y) 2 < 1

Tactic:
apply lt_of_le_of_ne y.cos_sq_le_one

Premises used: Real.cos_sq_le_one, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
rw : 1 - HPow.hPow (β := ℕ) (sin y) 2 ≠ 1
⊢ HPow.hPow (β := ℕ) (cos y) 2 ≠ 1

Tactic:
rw [cos_sq']

Premises used: Real.cos_sq'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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 (β := ℕ) (sin y) 2 ≠ 1

Tactic:
simpa only [Ne, sub_eq_self, sq_eq_zero_iff] using (sin_pos hy).ne'

Premises used: Ne, sub_eq_self, LT.lt.ne', sq_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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

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'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
hb : 0 < HPow.hPow (β := ℕ) (cos y) 2
⊢ 1 < (HPow.hPow (β := ℕ) (cos y) 2)⁻¹

Tactic:
rwa [lt_inv_comm₀, inv_one]

Premises used: inv_one, lt_inv_comm₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ LT.lt (α := ℝ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ LT.lt (α := ℝ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
⊢ 0 < HPow.hPow (β := ℕ) (cos y) 2

Tactic:
simpa only [sq, mul_self_pos] using this.ne'

Premises used: sq, mul_self_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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)

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'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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)
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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))
rwa rwa₁ rwa₂ rwa₃ : 0 < π / 2
⊢ 0 ∈ U

Tactic:
rwa [left_mem_Ico]

Premises used: Set.left_mem_Ico
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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))
⊢ 0 ∈ U

Tactic:
have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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 ∈ U

Tactic:
have x_in_U : x ∈ U := ⟨h1.le, h2⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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_in_U : x ∈ U
⊢ x < tan x

Tactic:
simpa only [tan_zero, sub_zero, sub_pos] using mono zero_in_U x_in_U h1

Premises used: sub_pos, sub_zero, Real.tan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
inl : ∀ (h1 : LE.le (α := ℝ) 0 0) (h2 : 0 < π / 2), 0 ≤ tan 0
inr : ∀ (h1' : 0 < x), x ≤ tan x
⊢ x ≤ tan x

Tactic:
rcases eq_or_lt_of_le h1 with (rfl | h1')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
h1 : LE.le (α := ℝ) 0 0
h2 : 0 < π / 2
inl inl₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ tan 0

Tactic:
rw [tan_zero]

Premises used: Real.tan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x

Tactic:
le_of_lt (lt_tan h1' h2)

Premises used: le_of_lt, Real.lt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x

Tactic:
exact le_of_lt (lt_tan h1' h2)

Premises used: le_of_lt, Real.lt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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)
inr : x < 0 → cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩

Premises used: Iff.mpr, Ne.symm, lt_or_lt_iff_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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 : 0 < x
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
this h hx2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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 : 0 < x
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
exact this h hx2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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
linarith₃ : -x ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₄ : -x ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
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 : ℝ
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 : 3 * π / 2 < -x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : 3 * π / 2 < -x → 2 / 2 = 1
linarith₂ : 3 * π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 3 * π / 2 < -x → GT.gt (α := ℝ) 2 0
linarith₄ : 3 * π / 2 < -x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : 3 * π / 2 < -x → 2 / 2 = 1
linarith₆ : 3 * π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : 3 * π / 2 < -x → GT.gt (α := ℝ) 2 0
linarith₈ : 3 * π / 2 < -x → HMul.hMul (α := ℝ) 1 1 = 1
linarith₉ : 3 * π / 2 < -x → 2 / 2 = 1
linarith₁₀ : 3 * π / 2 < -x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : 3 * π / 2 < -x → GT.gt (α := ℝ) 2 0
linarith₁₂ :
  3 * π / 2 < -x → -(HMul.hMul (α := ℝ) 1 3 * (1 * π)) - 2 * x + (HMul.hMul (α := ℝ) 1 3 * (1 * π) - -(2 * x)) = 0
⊢ -x ≤ 3 * π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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_1 : x < 0
h : cos x = cos (-x)
h₁ : 1 / √(HPow.hPow (β := ℕ) x 2 + 1) = 1 / √(HPow.hPow (β := ℕ) (-x) 2 + 1)
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
convert! this (by linarith : 0 < -x) (by linarith) using 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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_1 : x < 0
h h₁ : cos x = cos x
⊢ cos x = cos (-x)

Tactic:
rw [cos_neg]

Premises used: Real.cos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
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_1 : x < 0
h h₁ : 1 / √(HPow.hPow (β := ℕ) x 2 + 1) = 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
⊢ 1 / √(HPow.hPow (β := ℕ) x 2 + 1) = 1 / √(HPow.hPow (β := ℕ) (-x) 2 + 1)

Tactic:
rw [neg_sq]

Premises used: neg_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
suffices : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
⊢ cos x < 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
suffices ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1) by
    rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
    · exact this h hx2
    · convert! this (by linarith : 0 < -x) (by linarith) using 1
      · rw [cos_neg]
      · rw [neg_sq]