θ : Angle
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
θ : Angle
⊢ toReal θ < 0 ↔ sign θ = -1
rw [sign, ← sin_toReal, sign_eq_neg_one_iff]
case inl
θ : Angle
h : toReal θ < 0
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0

case inr.inl
θ : Angle
h : toReal θ = 0
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0

case inr.inr
θ : Angle
h : 0 < toReal θ
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
θ : Angle
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
rcases lt_trichotomy θ.toReal 0 with (h | h | h)
no goals
case inl
θ : Angle
h : toReal θ < 0
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
exact ⟨fun _ => Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_toReal θ), fun _ => h⟩
no goals
case inr.inl
θ : Angle
h : toReal θ = 0
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
simp [h]
no goals
case inr.inr
θ : Angle
h : 0 < toReal θ
⊢ toReal θ < 0 ↔ Real.sin (toReal θ) < 0
exact
  ⟨fun hn => False.elim (h.asymm hn), fun hn =>
    False.elim (hn.not_le (sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)))⟩