chore (Order.Defs): reorder parents to simplify instances and avoid non-reducible defeq checks (leanprover-community#9034)

Currently, `OrderDual.orderedCommMonoid` unifies with `LinearOrderedAddCommMonoid.toOrderedAddCommMonoid` at instance transparency because of an extra eta expansion in its definition. The provided instances can be synthesized by Lean and deleted. This removes the extraneous eta expansion but causes defeq to fail at instance transparency. To fix this, we reorder the parents of `LinearOrderedAddCommMonoid`. We also do this for the non-`Add` version.

Author: mattrobball

Mathlib/Algebra/Order/Monoid/Defs.lean

@@ -123,16 +123,14 @@ set_option linter.deprecated false in
 #align bit0_pos bit0_pos
 
 /-- A linearly ordered additive commutative monoid. -/
-class LinearOrderedAddCommMonoid (α : Type*) extends LinearOrder α, OrderedAddCommMonoid α
+class LinearOrderedAddCommMonoid (α : Type*) extends OrderedAddCommMonoid α, LinearOrder α
 #align linear_ordered_add_comm_monoid LinearOrderedAddCommMonoid
 
 /-- A linearly ordered commutative monoid. -/
 @[to_additive]
-class LinearOrderedCommMonoid (α : Type*) extends LinearOrder α, OrderedCommMonoid α
+class LinearOrderedCommMonoid (α : Type*) extends OrderedCommMonoid α, LinearOrder α
 #align linear_ordered_comm_monoid LinearOrderedCommMonoid
 
-attribute [to_additive existing] LinearOrderedCommMonoid.toOrderedCommMonoid
-
 /-- A linearly ordered cancellative additive commutative monoid is an additive commutative monoid
 with a decidable linear order in which addition is cancellative and monotone. -/
 class LinearOrderedCancelAddCommMonoid (α : Type*) extends OrderedCancelAddCommMonoid α,

Mathlib/Algebra/Order/Monoid/OrderDual.lean

@@ -81,8 +81,7 @@ instance covariantClass_swap_mul_lt [LT α] [Mul α]
 
 @[to_additive]
 instance orderedCommMonoid [OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ :=
-  { OrderDual.instPartialOrder α, OrderDual.instCommMonoid with
-    mul_le_mul_left := fun _ _ h c => mul_le_mul_left' h c }
+  { mul_le_mul_left := fun _ _ h c => mul_le_mul_left' h c }
 #align order_dual.ordered_comm_monoid OrderDual.orderedCommMonoid
 #align order_dual.ordered_add_comm_monoid OrderDual.orderedAddCommMonoid
 
@@ -99,8 +98,7 @@ instance OrderedCancelCommMonoid.to_contravariantClass [OrderedCancelCommMonoid
 
 @[to_additive]
 instance orderedCancelCommMonoid [OrderedCancelCommMonoid α] : OrderedCancelCommMonoid αᵒᵈ :=
-  { OrderDual.orderedCommMonoid, @OrderDual.instCancelCommMonoid α _ with
-    le_of_mul_le_mul_left := fun _ _ _ : α => le_of_mul_le_mul_left' }
+  { le_of_mul_le_mul_left := fun _ _ _ : α => le_of_mul_le_mul_left' }
 
 @[to_additive]
 instance linearOrderedCancelCommMonoid [LinearOrderedCancelCommMonoid α] :

Mathlib/RingTheory/Valuation/ValuationRing.lean

@@ -126,7 +126,7 @@ protected theorem le_total (a b : ValueGroup A K) : a ≤ b ∨ b ≤ a := by
 
 -- Porting note: it is much faster to split the instance `LinearOrderedCommGroupWithZero`
 -- into two parts
-noncomputable instance : LinearOrder (ValueGroup A K) where
+noncomputable instance linearOrder : LinearOrder (ValueGroup A K) where
   le_refl := by rintro ⟨⟩; use 1; rw [one_smul]
   le_trans := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨e, rfl⟩ ⟨f, rfl⟩; use e * f; rw [mul_smul]
   le_antisymm := by
@@ -146,33 +146,34 @@ noncomputable instance : LinearOrder (ValueGroup A K) where
   decidableLE := by classical infer_instance
 
 noncomputable instance linearOrderedCommGroupWithZero :
-    LinearOrderedCommGroupWithZero (ValueGroup A K) where
-  mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]; apply Setoid.refl'
-  one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]; apply Setoid.refl'
-  mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]; apply Setoid.refl'
-  mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]; apply Setoid.refl'
-  mul_le_mul_left := by
-    rintro ⟨a⟩ ⟨b⟩ ⟨c, rfl⟩ ⟨d⟩
-    use c; simp only [Algebra.smul_def]; ring
-  zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]; apply Setoid.refl'
-  mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]; apply Setoid.refl'
-  zero_le_one := ⟨0, by rw [zero_smul]⟩
-  exists_pair_ne := by
-    use 0, 1
-    intro c; obtain ⟨d, hd⟩ := Quotient.exact' c
-    apply_fun fun t => d⁻¹ • t at hd
-    simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd
-  inv_zero := by apply Quotient.sound'; rw [inv_zero]; apply Setoid.refl'
-  mul_inv_cancel := by
-    rintro ⟨a⟩ ha
-    apply Quotient.sound'
-    use 1
-    simp only [one_smul, ne_eq]
-    apply (mul_inv_cancel _).symm
-    contrapose ha
-    simp only [Classical.not_not] at ha ⊢
-    rw [ha]
-    rfl
+    LinearOrderedCommGroupWithZero (ValueGroup A K) :=
+  { linearOrder .. with
+    mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]; apply Setoid.refl'
+    one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]; apply Setoid.refl'
+    mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]; apply Setoid.refl'
+    mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]; apply Setoid.refl'
+    mul_le_mul_left := by
+      rintro ⟨a⟩ ⟨b⟩ ⟨c, rfl⟩ ⟨d⟩
+      use c; simp only [Algebra.smul_def]; ring
+    zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]; apply Setoid.refl'
+    mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]; apply Setoid.refl'
+    zero_le_one := ⟨0, by rw [zero_smul]⟩
+    exists_pair_ne := by
+      use 0, 1
+      intro c; obtain ⟨d, hd⟩ := Quotient.exact' c
+      apply_fun fun t => d⁻¹ • t at hd
+      simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd
+    inv_zero := by apply Quotient.sound'; rw [inv_zero]; apply Setoid.refl'
+    mul_inv_cancel := by
+      rintro ⟨a⟩ ha
+      apply Quotient.sound'
+      use 1
+      simp only [one_smul, ne_eq]
+      apply (mul_inv_cancel _).symm
+      contrapose ha
+      simp only [Classical.not_not] at ha ⊢
+      rw [ha]
+      rfl }
 
 /-- Any valuation ring induces a valuation on its fraction field. -/
 def valuation : Valuation K (ValueGroup A K) where