case inl
θ : Angle
h : toReal θ < 0
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ

case inr.inl
θ : Angle
h : toReal θ = 0
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ

case inr.inr
θ : Angle
h : 0 < toReal θ
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
θ : Angle
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
rcases lt_trichotomy θ.toReal 0 with (h | h | h)
case inl
θ : Angle
h : toReal θ < 0
hn : 0 ≤ sign θ
⊢ 0 ≤ toReal θ
case inl
θ : Angle
h : toReal θ < 0
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
refine' ⟨fun hn => False.elim (h.not_le hn), fun hn => _⟩
case inl
θ : Angle
h : toReal θ < 0
hn : 0 ≤ -1
⊢ 0 ≤ toReal θ
case inl
θ : Angle
h : toReal θ < 0
hn : 0 ≤ sign θ
⊢ 0 ≤ toReal θ
rw [toReal_neg_iff_sign_neg.1 h] at hn
no goals
case inl
θ : Angle
h : toReal θ < 0
hn : 0 ≤ -1
⊢ 0 ≤ toReal θ
exact False.elim (hn.not_lt (by decide))
no goals
θ : Angle
h : toReal θ < 0
hn : 0 ≤ -1
⊢ -1 < 0
decide
no goals
case inr.inl
θ : Angle
h : toReal θ = 0
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
simp [h, sign, ← sin_toReal]
case inr.inr
θ : Angle
h : 0 < toReal θ
x✝ : 0 ≤ toReal θ
⊢ 0 ≤ sign θ
case inr.inr
θ : Angle
h : 0 < toReal θ
⊢ 0 ≤ toReal θ ↔ 0 ≤ sign θ
refine' ⟨fun _ => _, fun _ => h.le⟩
case inr.inr
θ : Angle
h : 0 < toReal θ
x✝ : 0 ≤ toReal θ
⊢ 0 ≤ Real.sin (toReal θ)
case inr.inr
θ : Angle
h : 0 < toReal θ
x✝ : 0 ≤ toReal θ
⊢ 0 ≤ sign θ
rw [sign, ← sin_toReal, sign_nonneg_iff]
no goals
case inr.inr
θ : Angle
h : 0 < toReal θ
x✝ : 0 ≤ toReal θ
⊢ 0 ≤ Real.sin (toReal θ)
exact sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)