no goals
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
rcases lt_trichotomy x 0 with (hx | hx | hx) <;> rcases lt_trichotomy y 0 with (hy | hy | hy) <;>
  simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]