case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : x < 0
⊢ abs x * ↑(↑sign x) = x

case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ abs 0 * ↑(↑sign 0) = 0

case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : 0 < x
⊢ abs x * ↑(↑sign x) = x
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
⊢ abs x * ↑(↑sign x) = x
rcases lt_trichotomy x 0 with (hx | rfl | hx)
no goals
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : x < 0
⊢ abs x * ↑(↑sign x) = x
rw [sign_neg hx, abs_of_neg hx, coe_neg_one, mul_neg_one, neg_neg]
no goals
case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ abs 0 * ↑(↑sign 0) = 0
rw [abs_zero, zero_mul]
no goals
case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : 0 < x
⊢ abs x * ↑(↑sign x) = x
rw [sign_pos hx, abs_of_pos hx, coe_one, mul_one]