chore: Split Data.Pi.Lex (#13008)

... into
* `Order.PiLex` for the purely order theoretic constructions
* `Algebra.Order.Group.PiLex` for the algebraic order constructions

Counterexamples/MapFloor.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.Order.Hom.Ring
+import Mathlib.Algebra.Order.Group.PiLex
 import Mathlib.Algebra.Polynomial.Reverse
 
 #align_import map_floor from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"

Mathlib.lean

@@ -483,6 +483,7 @@ import Mathlib.Algebra.Order.Group.Lattice
 import Mathlib.Algebra.Order.Group.MinMax
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Order.Group.OrderIso
+import Mathlib.Algebra.Order.Group.PiLex
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Group.TypeTags
@@ -2128,7 +2129,6 @@ import Mathlib.Data.PNat.Xgcd
 import Mathlib.Data.PSigma.Order
 import Mathlib.Data.Part
 import Mathlib.Data.Pi.Interval
-import Mathlib.Data.Pi.Lex
 import Mathlib.Data.Prod.Basic
 import Mathlib.Data.Prod.Lex
 import Mathlib.Data.Prod.PProd
@@ -3281,6 +3281,7 @@ import Mathlib.Order.PFilter
 import Mathlib.Order.PartialSups
 import Mathlib.Order.Partition.Equipartition
 import Mathlib.Order.Partition.Finpartition
+import Mathlib.Order.PiLex
 import Mathlib.Order.PrimeIdeal
 import Mathlib.Order.PrimeSeparator
 import Mathlib.Order.PropInstances

Mathlib/Algebra/Order/Group/PiLex.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Mathlib.Algebra.Group.OrderSynonym
+import Mathlib.Algebra.Group.Pi.Basic
+import Mathlib.Algebra.Order.Group.Defs
+import Mathlib.Order.PiLex
+
+/-!
+# Lexicographic product of algebraic order structures
+
+This file proves that the lexicographic order on pi types is compatible with the pointwise algebraic
+operations.
+-/
+
+namespace Pi.Lex
+variable {ι : Type*} {α : ι → Type*} [LinearOrder ι]
+
+@[to_additive]
+instance orderedCancelCommMonoid [∀ i, OrderedCancelCommMonoid (α i)] :
+    OrderedCancelCommMonoid (Lex (∀ i, α i)) where
+  mul_le_mul_left _ _ hxy z :=
+    hxy.elim (fun hxyz => hxyz ▸ le_rfl) fun ⟨i, hi⟩ =>
+      Or.inr ⟨i, fun j hji => congr_arg (z j * ·) (hi.1 j hji), mul_lt_mul_left' hi.2 _⟩
+  le_of_mul_le_mul_left _ _ _ hxyz :=
+    hxyz.elim (fun h => (mul_left_cancel h).le) fun ⟨i, hi⟩ =>
+      Or.inr ⟨i, fun j hj => (mul_left_cancel <| hi.1 j hj), lt_of_mul_lt_mul_left' hi.2⟩
+
+@[to_additive]
+instance orderedCommGroup [∀ i, OrderedCommGroup (α i)] : OrderedCommGroup (Lex (∀ i, α i)) where
+  mul_le_mul_left _ _ := mul_le_mul_left'
+#align pi.lex.ordered_comm_group Pi.Lex.orderedCommGroup
+#align pi.lex.ordered_add_comm_group Pi.Lex.orderedAddCommGroup
+
+@[to_additive]
+noncomputable instance linearOrderedCancelCommMonoid [IsWellOrder ι (· < ·)]
+    [∀ i, LinearOrderedCancelCommMonoid (α i)] :
+    LinearOrderedCancelCommMonoid (Lex (∀ i, α i)) where
+  __ : LinearOrder (Lex (∀ i, α i)) := inferInstance
+  __ : OrderedCancelCommMonoid (Lex (∀ i, α i)) := inferInstance
+
+@[to_additive]
+noncomputable instance linearOrderedCommGroup [IsWellOrder ι (· < ·)]
+    [∀ i, LinearOrderedCommGroup (α i)] :
+    LinearOrderedCommGroup (Lex (∀ i, α i)) where
+  __ : LinearOrder (Lex (∀ i, α i)) := inferInstance
+  mul_le_mul_left _ _ := mul_le_mul_left'
+
+end Pi.Lex

Mathlib/Data/DFinsupp/Lex.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Junyan Xu
 -/
+import Mathlib.Algebra.Order.Group.PiLex
 import Mathlib.Data.DFinsupp.Order
 import Mathlib.Data.DFinsupp.NeLocus
 import Mathlib.Order.WellFoundedSet

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Yury Kudryashov, Sébastien Gouëzel, Chris Hughes
 -/
 import Mathlib.Data.Fin.OrderHom
-import Mathlib.Data.Pi.Lex
+import Mathlib.Order.PiLex
 import Mathlib.Order.Interval.Set.Basic
 
 #align_import data.fin.tuple.basic from "leanprover-community/mathlib"@"ef997baa41b5c428be3fb50089a7139bf4ee886b"

Mathlib/Data/Pi/Lex.lean → Mathlib/Order/PiLex.lean

@@ -3,11 +3,8 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.Algebra.Group.OrderSynonym
-import Mathlib.Algebra.Group.Pi.Basic
-import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Order.WellFounded
-import Mathlib.Mathport.Notation
+import Mathlib.Tactic.Common
 
 #align_import data.pi.lex from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1"
 
@@ -31,6 +28,7 @@ Related files are:
 * `Data.Prod.Lex`: Lexicographic order on `α × β`.
 -/
 
+assert_not_exists Monoid
 
 variable {ι : Type*} {β : ι → Type*} (r : ι → ι → Prop) (s : ∀ {i}, β i → β i → Prop)
 
@@ -219,43 +217,6 @@ instance [LinearOrder ι] [IsWellOrder ι (· < ·)] [Nonempty ι] [∀ i, Parti
     let ⟨_, hb⟩ := exists_lt (ofLex a)
     ⟨_, toLex_strictMono hb⟩⟩
 
-section OrderedMonoid
-
-variable [LinearOrder ι]
-
-@[to_additive]
-instance Lex.orderedCancelCommMonoid [∀ i, OrderedCancelCommMonoid (β i)] :
-    OrderedCancelCommMonoid (Lex (∀ i, β i)) where
-  mul_le_mul_left _ _ hxy z :=
-    hxy.elim (fun hxyz => hxyz ▸ le_rfl) fun ⟨i, hi⟩ =>
-      Or.inr ⟨i, fun j hji => congr_arg (z j * ·) (hi.1 j hji), mul_lt_mul_left' hi.2 _⟩
-  le_of_mul_le_mul_left _ _ _ hxyz :=
-    hxyz.elim (fun h => (mul_left_cancel h).le) fun ⟨i, hi⟩ =>
-      Or.inr ⟨i, fun j hj => (mul_left_cancel <| hi.1 j hj), lt_of_mul_lt_mul_left' hi.2⟩
-
-@[to_additive]
-instance Lex.orderedCommGroup [∀ i, OrderedCommGroup (β i)] :
-    OrderedCommGroup (Lex (∀ i, β i)) where
-  mul_le_mul_left _ _ := mul_le_mul_left'
-#align pi.lex.ordered_comm_group Pi.Lex.orderedCommGroup
-#align pi.lex.ordered_add_comm_group Pi.Lex.orderedAddCommGroup
-
-@[to_additive]
-noncomputable instance Lex.linearOrderedCancelCommMonoid [IsWellOrder ι (· < ·)]
-    [∀ i, LinearOrderedCancelCommMonoid (β i)] :
-    LinearOrderedCancelCommMonoid (Lex (∀ i, β i)) where
-  __ : LinearOrder (Lex (∀ i, β i)) := inferInstance
-  __ : OrderedCancelCommMonoid (Lex (∀ i, β i)) := inferInstance
-
-@[to_additive]
-noncomputable instance Lex.linearOrderedCommGroup [IsWellOrder ι (· < ·)]
-    [∀ i, LinearOrderedCommGroup (β i)] :
-    LinearOrderedCommGroup (Lex (∀ i, β i)) where
-  __ : LinearOrder (Lex (∀ i, β i)) := inferInstance
-  mul_le_mul_left _ _ := mul_le_mul_left'
-
-end OrderedMonoid
-
 /-- If we swap two strictly decreasing values in a function, then the result is lexicographically
 smaller than the original function. -/
 theorem lex_desc {α} [Preorder ι] [DecidableEq ι] [Preorder α] {f : ι → α} {i j : ι} (h₁ : i ≤ j)