[GOAL]
x : ℝ
h : 0 < x
⊢ sin x < x
[PROOFSTEP]
cases' lt_or_le 1 x with h' h'
[GOAL]
case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x
[PROOFSTEP]
exact (sin_le_one x).trans_lt h'
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < x
[PROOFSTEP]
have hx : |x| = x := abs_of_nonneg h.le
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ sin x < x
[PROOFSTEP]
have := le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1
[PROOFSTEP]
rwa [hx]
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x - (x - x ^ 3 / 6) ≤ |x| ^ 4 * (5 / 96)
⊢ sin x < x
[PROOFSTEP]
rw [sub_le_iff_le_add', hx] at this 
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ sin x < x
[PROOFSTEP]
apply this.trans_lt
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x
[PROOFSTEP]
rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹
[PROOFSTEP]
refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 5 / 96 < 6⁻¹
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 0 ≤ 5 / 96
[PROOFSTEP]
norm_num
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 ≤ x ^ 3
[PROOFSTEP]
apply pow_le_pow_of_le_one h.le h'
[GOAL]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 3 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
have hx : |x| = x := abs_of_nonneg h.le
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1
[PROOFSTEP]
rwa [hx]
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(|x| ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
rw [le_sub_iff_add_le, hx] at this 
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < sin x
[PROOFSTEP]
refine' lt_of_lt_of_le _ this
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)
[PROOFSTEP]
have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by ring
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
[PROOFSTEP]
ring
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)
[PROOFSTEP]
rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 12⁻¹
[PROOFSTEP]
refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 5 / 96 < 12⁻¹
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 0 ≤ 5 / 96
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 ≤ x ^ 3
[PROOFSTEP]
apply pow_le_pow_of_le_one h.le h'
[GOAL]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 3 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt (fun y => tan y - y) (↑1 / cos x ^ 2 - 1) x
[PROOFSTEP]
simpa using (hasDerivAt_tan h).add (hasDerivAt_id x).neg
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
⊢ x < tan x
[PROOFSTEP]
let U := Ico 0 (π / 2)
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
⊢ x < tan x
[PROOFSTEP]
have intU : interior U = Ioo 0 (π / 2) := interior_Ico
[GOAL]
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
⊢ x < tan x
[PROOFSTEP]
have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
[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
[PROOFSTEP]
have cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y := by
  intro y hy
  exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
[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 : ℝ}, y ∈ U → 0 < cos y
[PROOFSTEP]
intro y hy
[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
[PROOFSTEP]
exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
[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 : ℝ}, y ∈ U → 0 < cos y
⊢ x < tan x
[PROOFSTEP]
have sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y :=
  by
  intro y hy
  rw [intU] at hy 
  exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
[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 : ℝ}, y ∈ U → 0 < cos y
⊢ ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
[PROOFSTEP]
intro y hy
[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 : ℝ}, y ∈ U → 0 < cos y
y : ℝ
hy : y ∈ interior U
⊢ 0 < sin y
[PROOFSTEP]
rw [intU] at hy 
[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 : ℝ}, y ∈ U → 0 < cos y
y : ℝ
hy : y ∈ Ioo 0 (π / 2)
⊢ 0 < sin y
[PROOFSTEP]
exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ x < tan x
[PROOFSTEP]
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'
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ ContinuousOn tan U
[PROOFSTEP]
apply ContinuousOn.mono continuousOn_tan
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ U ⊆ {x | cos x ≠ 0}
[PROOFSTEP]
intro z hz
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
z : ℝ
hz : z ∈ U
⊢ z ∈ {x | cos x ≠ 0}
[PROOFSTEP]
simp only [mem_setOf_eq]
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
z : ℝ
hz : z ∈ U
⊢ cos z ≠ 0
[PROOFSTEP]
exact (cos_pos hz).ne'
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
⊢ x < tan x
[PROOFSTEP]
have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
⊢ x < tan x
[PROOFSTEP]
have deriv_pos : ∀ y : ℝ, y ∈ interior U → 0 < deriv (fun y' : ℝ => tan y' - y') y :=
  by
  intro y hy
  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.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne'
  rwa [one_div, lt_inv, inv_one]
  · exact zero_lt_one
  simpa only [sq, mul_self_pos] using this.ne'
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
⊢ ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
[PROOFSTEP]
intro y hy
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
⊢ 0 < deriv (fun y' => tan y' - y') y
[PROOFSTEP]
have := cos_pos (interior_subset hy)
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 0 < deriv (fun y' => tan y' - y') y
[PROOFSTEP]
simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 < ↑1 / cos y ^ 2
[PROOFSTEP]
norm_cast
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 < 1 / cos y ^ 2
[PROOFSTEP]
have bd2 : cos y ^ 2 < 1 := by
  apply lt_of_le_of_ne y.cos_sq_le_one
  rw [cos_sq']
  simpa only [Ne.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne'
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ cos y ^ 2 < 1
[PROOFSTEP]
apply lt_of_le_of_ne y.cos_sq_le_one
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ cos y ^ 2 ≠ 1
[PROOFSTEP]
rw [cos_sq']
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 - sin y ^ 2 ≠ 1
[PROOFSTEP]
simpa only [Ne.def, sub_eq_self, pow_eq_zero_iff, Nat.succ_pos'] using (sin_pos hy).ne'
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : cos y ^ 2 < 1
⊢ 1 < 1 / cos y ^ 2
[PROOFSTEP]
rwa [one_div, lt_inv, inv_one]
[GOAL]
case ha
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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : cos y ^ 2 < 1
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case hb
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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
bd2 : cos y ^ 2 < 1
⊢ 0 < cos y ^ 2
[PROOFSTEP]
simpa only [sq, mul_self_pos] using this.ne'
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
⊢ x < tan x
[PROOFSTEP]
have mono := Convex.strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))
⊢ x < tan x
[PROOFSTEP]
have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 0 < deriv (fun y' => tan y' - y') y
mono : StrictMonoOn (fun y => tan y - y) (Ico 0 (π / 2))
⊢ 0 ∈ U
[PROOFSTEP]
rwa [left_mem_Ico]
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 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
[PROOFSTEP]
have x_in_U : x ∈ U := ⟨h1.le, h2⟩
[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 : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y => tan y - y) U
deriv_pos : ∀ (y : ℝ), y ∈ interior U → 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
[PROOFSTEP]
simpa only [tan_zero, sub_zero, sub_pos] using mono zero_in_U x_in_U h1
[GOAL]
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x
[PROOFSTEP]
rcases eq_or_lt_of_le h1 with (rfl | h1')
[GOAL]
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0
[PROOFSTEP]
rw [tan_zero]
[GOAL]
case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x
[PROOFSTEP]
exact le_of_lt (lt_tan h1' h2)
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
suffices ∀ {y : ℝ} (_ : 0 < y) (_ : y ≤ 3 * π / 2), cos y < ↑1 / sqrt (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]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h : 0 < x
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
exact this h hx2
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ cos x < 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
convert this (by linarith : 0 < -x) (by linarith) using 1
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ 0 < -x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ -x ≤ 3 * π / 2
[PROOFSTEP]
linarith
[GOAL]
case h.e'_3
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ cos x = cos (-x)
[PROOFSTEP]
rw [cos_neg]
[GOAL]
case h.e'_4
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
h✝ : x < 0
⊢ 1 / sqrt (x ^ 2 + 1) = 1 / sqrt ((-x) ^ 2 + 1)
[PROOFSTEP]
rw [neg_sq]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
intro y hy1 hy2
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
have hy3 : ↑0 < y ^ 2 + 1 := by linarith [sq_nonneg y]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ 0 < y ^ 2 + 1
[PROOFSTEP]
linarith [sq_nonneg y]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
rcases lt_or_le y (π / 2) with (hy2' | hy1')
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
have hy4 : 0 < cos y := cos_pos_of_mem_Ioo ⟨by linarith, hy2'⟩
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
⊢ -(π / 2) < y
[PROOFSTEP]
linarith
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
rw [← abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨by linarith, hy2'.le⟩), ←
  abs_of_nonneg (one_div_nonneg.mpr (sqrt_nonneg _)), ← sq_lt_sq, div_pow, one_pow, sq_sqrt hy3.le,
  lt_one_div (pow_pos hy4 _) hy3, ← inv_one_add_tan_sq hy4.ne', one_div, inv_inv, add_comm, add_lt_add_iff_left,
  sq_lt_sq, abs_of_pos hy1, abs_of_nonneg (tan_nonneg_of_nonneg_of_le_pi_div_two hy1.le hy2'.le)]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ -(π / 2) ≤ y
[PROOFSTEP]
linarith
[GOAL]
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y < tan y
[PROOFSTEP]
exact Real.lt_tan hy1 hy2'
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ cos y < 1 / sqrt (y ^ 2 + 1)
[PROOFSTEP]
refine' lt_of_le_of_lt _ (one_div_pos.mpr <| sqrt_pos_of_pos hy3)
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ cos y ≤ 0
[PROOFSTEP]
exact cos_nonpos_of_pi_div_two_le_of_le hy1' (by linarith [pi_pos])
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ y ≤ π + π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx3)
[GOAL]
case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / sqrt (0 ^ 2 + 1)
[PROOFSTEP]
simp
[GOAL]
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
[PROOFSTEP]
exact (cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le
