chore: revert reducibility change PartialOrder.rel

This PR is similar to #12403.

We previously conjectured that "all type class fields that are types
should be marked as reducible." The problem is that propositions are
types, but they are also used as data (with `Decidable`).
For example, we often see the proposition `x <= y` as a Boolean.
So, we refined the conjecture to:

"All type class fields that are types (and not propositions) should be marked as reducible."

src/Init/Internal/Order/Basic.lean

@@ -50,8 +50,6 @@ class PartialOrder (α : Sort u) where
   /-- The “less-or-equal-to” or “approximates” relation is antisymmetric. -/
   rel_antisymm : ∀ {x y}, rel x y → rel y x → x = y
 
-attribute [reducible] PartialOrder.rel
-
 @[inherit_doc] scoped infix:50 " ⊑ " => PartialOrder.rel
 
 section PartialOrder