θ : Angle
h : sign θ = -1 ∨ sign θ = 0
⊢ -↑(abs (toReal θ)) = θ
θ : Angle
h : sign θ ≤ 0
⊢ -↑(abs (toReal θ)) = θ
rw [SignType.nonpos_iff] at h
case inl
θ : Angle
h : sign θ = -1
⊢ -↑(abs (toReal θ)) = θ

case inr
θ : Angle
h : sign θ = 0
⊢ -↑(abs (toReal θ)) = θ
θ : Angle
h : sign θ = -1 ∨ sign θ = 0
⊢ -↑(abs (toReal θ)) = θ
rcases h with (h | h)
no goals
case inl
θ : Angle
h : sign θ = -1
⊢ -↑(abs (toReal θ)) = θ
rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑(abs (toReal θ)) = θ
case inr
θ : Angle
h : sign θ = 0
⊢ -↑(abs (toReal θ)) = θ
rw [sign_eq_zero_iff] at h
no goals
case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑(abs (toReal θ)) = θ
rcases h with (rfl | rfl) <;> simp [abs_of_pos Real.pi_pos]