case inl
θ : Angle
h : θ ≠ ↑π
ht : toReal θ < 0
⊢ ↑SignType.sign (toReal θ) = sign θ

case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : toReal θ = 0
⊢ ↑SignType.sign (toReal θ) = sign θ

case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < toReal θ
⊢ ↑SignType.sign (toReal θ) = sign θ
θ : Angle
h : θ ≠ ↑π
⊢ ↑SignType.sign (toReal θ) = sign θ
rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
no goals
case inl
θ : Angle
h : θ ≠ ↑π
ht : toReal θ < 0
⊢ ↑SignType.sign (toReal θ) = sign θ
simp [ht, toReal_neg_iff_sign_neg.1 ht]
no goals
case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : toReal θ = 0
⊢ ↑SignType.sign (toReal θ) = sign θ
simp [sign, ht, ← sin_toReal]
no goals
case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < toReal θ
⊢ ↑SignType.sign (toReal θ) = sign θ
rw [sign, ← sin_toReal, sign_pos ht,
  sign_pos
    (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]