θ : Angle
⊢ 0 ≤ cos ↑(toReal θ) ↔ abs (toReal θ) ≤ π / 2
θ : Angle
⊢ 0 ≤ cos θ ↔ abs (toReal θ) ≤ π / 2
nth_rw 1 [← coe_toReal θ]
θ : Angle
⊢ 0 ≤ Real.cos (toReal θ) ↔ -(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2
θ : Angle
⊢ 0 ≤ cos ↑(toReal θ) ↔ abs (toReal θ) ≤ π / 2
rw [abs_le, cos_coe]
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
⊢ -(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2
θ : Angle
⊢ 0 ≤ Real.cos (toReal θ) ↔ -(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2
refine' ⟨fun h => _, cos_nonneg_of_mem_Icc⟩
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : ¬(-(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2)
⊢ False
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
⊢ -(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2
by_contra hn
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2) ∨ π / 2 < toReal θ
⊢ False
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : ¬(-(π / 2) ≤ toReal θ ∧ toReal θ ≤ π / 2)
⊢ False
rw [not_and_or, not_le, not_le] at hn
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2) ∨ π / 2 < toReal θ
⊢ Real.cos (toReal θ) < 0
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2) ∨ π / 2 < toReal θ
⊢ False
refine' (not_lt.2 h) _
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ Real.cos (toReal θ) < 0

case inr
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : π / 2 < toReal θ
⊢ Real.cos (toReal θ) < 0
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2) ∨ π / 2 < toReal θ
⊢ Real.cos (toReal θ) < 0
rcases hn with (hn | hn)
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ Real.cos (-toReal θ) < 0
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ Real.cos (toReal θ) < 0
rw [← Real.cos_neg]
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ -toReal θ < π + π / 2
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ Real.cos (-toReal θ) < 0
refine' cos_neg_of_pi_div_two_lt_of_lt (by linarith) _
no goals
case inl
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ -toReal θ < π + π / 2
linarith [neg_pi_lt_toReal θ]
no goals
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : toReal θ < -(π / 2)
⊢ π / 2 < -toReal θ
linarith
case inr
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : π / 2 < toReal θ
⊢ toReal θ < π + π / 2
case inr
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : π / 2 < toReal θ
⊢ Real.cos (toReal θ) < 0
refine' cos_neg_of_pi_div_two_lt_of_lt hn _
no goals
case inr
θ : Angle
h : 0 ≤ Real.cos (toReal θ)
hn : π / 2 < toReal θ
⊢ toReal θ < π + π / 2
linarith [toReal_le_pi θ]