lower instance priorities, add scoped higher prio versions

Mathlib/Algebra/Order/Field/Defs.lean

@@ -26,6 +26,8 @@ A linear ordered (semi)field is a (semi)field equipped with a linear order such
 -- Guard against import creep.
 assert_not_exists MonoidHom
 
+open scoped AlgebraOrderInstances
+
 variable {α : Type*}
 
 /-- A linear ordered semifield is a field with a linear order respecting the operations. -/
@@ -101,3 +103,13 @@ lemma zpow_pos_of_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
   | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _
   | -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _
 #align zpow_pos_of_pos zpow_pos_of_pos
+
+-- lower instance priorities to avoid instance synthesis trying this early
+attribute [instance 50] LinearOrderedSemifield.toSemifield
+attribute [instance 50] LinearOrderedField.toField
+
+-- add higer-priority versions in scope `AlgebraOrderInstances`
+namespace AlgebraOrderInstances
+attribute [scoped instance 1000] LinearOrderedSemifield.toSemifield
+attribute [scoped instance 1000] LinearOrderedField.toField
+end AlgebraOrderInstances

Mathlib/Algebra/Order/Group/Defs.lean

@@ -21,6 +21,7 @@ may differ between the multiplicative and the additive version of a lemma.
 The reason is that we did not want to change existing names in the library.
 -/
 
+open scoped AlgebraOrderInstances
 
 open Function
 
@@ -1291,6 +1292,18 @@ theorem StrictAntiOn.inv (hf : StrictAntiOn f s) : StrictMonoOn (fun x => (f x)
 
 end
 
+-- lower instance priorities to avoid instance synthesis trying this early
+attribute [instance 50] OrderedAddCommGroup.toAddCommGroup
+attribute [instance 50] OrderedCommGroup.toCommGroup
+attribute [instance 50] LinearOrderedAddCommGroupWithTop.toSubNegMonoid
+
+-- add higer-priority versions in scope `AlgebraOrderInstances`
+namespace AlgebraOrderInstances
+attribute [scoped instance 1000] OrderedAddCommGroup.toAddCommGroup
+attribute [scoped instance 1000] OrderedCommGroup.toCommGroup
+attribute [scoped instance 1000] LinearOrderedAddCommGroupWithTop.toSubNegMonoid
+end AlgebraOrderInstances
+
 /-
 `NeZero` should not be needed at this point in the ordered algebraic hierarchy.
 -/

Mathlib/Algebra/Order/Group/Units.lean

@@ -13,6 +13,7 @@ import Mathlib.Algebra.Order.Monoid.Units
 # The units of an ordered commutative monoid form an ordered commutative group
 -/
 
+open scoped AlgebraOrderInstances
 
 variable {α : Type*}
 

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -31,6 +31,8 @@ whereas it is a very common target for valuations.
 The solutions is to use a typeclass, and that is exactly what we do in this file.
 -/
 
+open scoped AlgebraOrderInstances
+
 variable {α : Type*}
 
 /-- A linearly ordered commutative monoid with a zero element. -/
@@ -470,3 +472,13 @@ instance instLinearOrderedCommGroupWithZero [LinearOrderedCommGroup α] :
   __ := commGroupWithZero
 
 end WithZero
+
+-- lower instance priorities to avoid instance synthesis trying this early
+attribute [instance 50] LinearOrderedCommMonoidWithZero.toCommMonoidWithZero
+attribute [instance 50] LinearOrderedCommGroupWithZero.toCommGroupWithZero
+
+-- add higer-priority versions in scope `AlgebraOrderInstances`
+namespace AlgebraOrderInstances
+attribute [scoped instance 1000] LinearOrderedCommMonoidWithZero.toCommMonoidWithZero
+attribute [scoped instance 1000] LinearOrderedCommGroupWithZero.toCommGroupWithZero
+end AlgebraOrderInstances

Mathlib/Algebra/Order/Monoid/Basic.lean

@@ -15,6 +15,7 @@ import Mathlib.Order.Hom.Basic
 This file develops some additional material on ordered monoids.
 -/
 
+open scoped AlgebraOrderInstances
 
 open Function
 

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -14,6 +14,8 @@ import Mathlib.Algebra.Order.Monoid.Defs
 # Canonically ordered monoids
 -/
 
+open scoped AlgebraOrderInstances
+
 universe u
 
 variable {α : Type u}

Mathlib/Algebra/Order/Monoid/Defs.lean

@@ -186,3 +186,13 @@ theorem mul_self_le_one_iff : a * a ≤ 1 ↔ a ≤ 1 := by simp [← not_iff_no
 
 @[to_additive (attr := simp)]
 theorem mul_self_lt_one_iff : a * a < 1 ↔ a < 1 := by simp [← not_iff_not]
+
+-- lower instance priorities to avoid instance synthesis trying this early
+attribute [instance 50] OrderedAddCommMonoid.toAddCommMonoid
+attribute [instance 50] OrderedCommMonoid.toCommMonoid
+
+-- add higer-priority versions in scope `AlgebraOrderInstances`
+namespace AlgebraOrderInstances
+attribute [scoped instance 1000] OrderedAddCommMonoid.toAddCommMonoid
+attribute [scoped instance 1000] OrderedCommMonoid.toCommMonoid
+end AlgebraOrderInstances

Mathlib/Algebra/Order/Monoid/OrderDual.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.Order.Monoid.Defs
 
 /-! # Ordered monoid structures on the order dual. -/
 
+open scoped AlgebraOrderInstances
 
 universe u
 

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -106,6 +106,8 @@ immediate predecessors and what conditions are added to each of them.
   - `CommRing` & `IsDomain` & linear order structure
 -/
 
+open scoped AlgebraOrderInstances
+
 open Function
 
 universe u
@@ -1327,4 +1329,28 @@ instance (priority := 100) LinearOrderedCommRing.toLinearOrderedCommSemiring
 @[deprecated] alias zero_lt_mul_left := mul_pos_iff_of_pos_left
 @[deprecated] alias zero_lt_mul_right := mul_pos_iff_of_pos_right
 
+-- lower instance priorities to avoid instance synthesis trying this early
+attribute [instance 50] OrderedSemiring.toSemiring
+attribute [instance 50] OrderedCommSemiring.toCommSemiring
+attribute [instance 50] OrderedRing.toRing
+attribute [instance 50] OrderedCommRing.toCommRing
+attribute [instance 50] StrictOrderedSemiring.toSemiring
+attribute [instance 50] StrictOrderedCommSemiring.toCommSemiring
+attribute [instance 50] StrictOrderedRing.toRing
+attribute [instance 50] StrictOrderedCommRing.toCommRing
+attribute [instance 50] LinearOrderedCommRing.toCommMonoid
+
+-- add higer-priority versions in scope `AlgebraOrderInstances`
+namespace AlgebraOrderInstances
+attribute [scoped instance 1000] OrderedSemiring.toSemiring
+attribute [scoped instance 1000] OrderedCommSemiring.toCommSemiring
+attribute [scoped instance 1000] OrderedRing.toRing
+attribute [scoped instance 1000] OrderedCommRing.toCommRing
+attribute [scoped instance 1000] StrictOrderedSemiring.toSemiring
+attribute [scoped instance 1000] StrictOrderedCommSemiring.toCommSemiring
+attribute [scoped instance 1000] StrictOrderedRing.toRing
+attribute [scoped instance 1000] StrictOrderedCommRing.toCommRing
+attribute [scoped instance 1000] LinearOrderedCommRing.toCommMonoid
+end AlgebraOrderInstances
+
 assert_not_exists MonoidHom