Squashed commit of the following:

commit d51b84d
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Jan 6 20:13:26 2026 +1100

    OrderIso prod lemmas adjustment

commit 4c41035
Merge: b88c734 15f6691
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Jan 6 20:04:32 2026 +1100

    Merge branch 'master' into master

commit b88c734
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Jan 6 19:33:15 2026 +1100

    Changes from review

commit 8252446
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Jan 6 16:00:09 2026 +1100

    Apply suggestions from code review

    Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

commit 8ac8458
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Jan 6 01:11:04 2026 +1100

    Change mathlib imports from `OrderType`

    `OrderType.lean` no longer exists

commit f353fe8
Merge: 30bd77d 959c852
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 23:17:21 2026 +1100

    Merge branch 'leanprover-community:master' into master

commit 30bd77d
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 21:49:57 2026 +1100

    Refactor as per suggestions, back to `LinOrd`

commit f8cd844
Merge: f04b327 a57b343
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 21:49:30 2026 +1100

    Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278

commit f04b327
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 11:36:50 2026 +1100

    Apply suggestions

commit a57b343
Merge: 5937b50 8c8bf56
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 11:30:56 2026 +1100

    Merge branch 'leanprover-community:master' into master

commit 5937b50
Merge: 07abc73 2330302
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 10:21:08 2026 +1100

    Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278

commit 2330302
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 10:20:45 2026 +1100

    Apply suggestions from code review

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

commit 07abc73
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 00:44:02 2026 +1100

    Fix recommended_spellings

commit b25cb4c
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 00:37:52 2026 +1100

    Add doc-string and some more typos

commit 067b8cd
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Jan 5 00:31:32 2026 +1100

    Minor typos

commit 4b5a837
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sun Jan 4 22:26:24 2026 +1100

    Finish conversation review suggestions

commit 5429c1b
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Jan 2 23:31:29 2026 +1100

    Apply suggestions from code review

    [skip ci]

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

commit 630f0ea
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Jan 2 23:14:37 2026 +1100

    Style fix

commit bf5166d
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Jan 2 22:58:10 2026 +1100

    Fix module error

commit 2f0a005
Merge: 44753fe 519f454
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Jan 2 20:11:02 2026 +1100

    Merge branch 'leanprover-community:master' into master

commit 44753fe
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Jan 2 19:42:27 2026 +1100

    Bump

commit 43b7d68
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Jan 2 19:18:34 2026 +1100

    Clean up imports, get rid of sorries, and address some comments

commit f888e2b
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Jan 1 22:12:33 2026 +1100

    Update OrderType.lean

    Add copyright
    [skip actions]

commit 9848662
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Jan 1 21:56:01 2026 +1100

    Update OrderType.lean

commit b8acc2e
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Jan 1 20:15:25 2026 +1100

    Apply suggestions from code review

    Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

commit a5e62be
Merge: 6aa39b3 de80207
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Wed Dec 31 16:34:44 2025 +1100

    Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278

commit 6aa39b3
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Wed Dec 31 16:34:33 2025 +1100

    Update OrderType.lean

commit de80207
Merge: 669a1d3 6dc6d70
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Wed Dec 31 16:34:24 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 669a1d3
Merge: a90d529 6371049
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Dec 29 10:38:08 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit a90d529
Merge: 24bb5b0 cc5691d
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Dec 22 13:06:26 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 24bb5b0
Merge: 4985680 5334b1e
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Wed Nov 26 18:44:18 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 4985680
Merge: 711df94 3f87ea8
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sun Nov 23 12:48:18 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 711df94
Merge: 6534400 b3cf7a0
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sat Nov 22 13:48:50 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit 6534400
Merge: bb1a642 56c98a5
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Nov 20 18:46:50 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit bb1a642
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Oct 20 21:27:21 2025 +1100

    Update OrderType.lean

commit f427a91
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Oct 20 18:25:16 2025 +1100

    Update OrderType.lean

commit f6c13a0
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Oct 20 17:59:56 2025 +1100

    Update OrderType.lean

commit 78e4c9a
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Mon Oct 20 16:29:31 2025 +1100

    Update OrderType.lean

commit e827b3c
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sat Oct 18 00:41:45 2025 +1100

    Update OrderType.lean

commit f5d5427
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sat Oct 18 00:23:18 2025 +1100

    Update OrderType.lean

commit 871acb9
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Oct 17 22:32:05 2025 +1100

    Update OrderType.lean

commit 803ced6
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Fri Oct 17 20:45:37 2025 +1100

    Update OrderType.lean

commit 2883e90
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Oct 16 23:04:21 2025 +1100

    Update OrderType.lean

commit 971c382
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Oct 16 23:02:18 2025 +1100

    Update OrderType.lean

commit 3db4465
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Oct 16 23:01:46 2025 +1100

    Update OrderType.lean

commit 3e7c325
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Thu Oct 16 22:59:05 2025 +1100

    Update OrderType.lean

commit ce284fa
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Oct 14 20:26:41 2025 +1100

    Update OrderType.lean

commit e0e79c8
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Oct 14 19:02:32 2025 +1100

    Create OrderTypes file with definition and some generalisation from Ordinal

commit e78fa58
Merge: aa54d18 3aa3aca
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Tue Oct 14 19:02:04 2025 +1100

    Merge branch 'leanprover-community:master' into master

commit aa54d18
Merge: 3742a3b efcc0aa
Author: Yan Yablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sun Sep 21 15:21:45 2025 +1000

    Merge branch 'leanprover-community:master' into master

commit 3742a3b
Author: YanYablonovskiy <yablonovskiy.yan@gmail.com>
Date:   Sat Sep 20 22:28:23 2025 +1000

    Create OrderTypes_basic.lean

Author: YanYablonovskiy

Mathlib/Data/Sum/Order.lean

@@ -717,6 +717,12 @@ theorem sumLexDualAntidistrib_symm_inr :
     (sumLexDualAntidistrib α β).symm (inr (toDual a)) = toDual (inl a) :=
   rfl
 
+def sumLexEmpty (α β : Type*) [Preorder α] [IsEmpty β] [Preorder β] :
+    Lex (α ⊕ β) ≃o α := @RelIso.sumLexEmpty α β _ _ _
+
+def emptySumLex (α β : Type*) [Preorder α] [IsEmpty β] [Preorder β] :
+    Lex (β ⊕ α) ≃o α := @RelIso.emptySumLex β α _ _ _
+
 end OrderIso
 
 variable [LE α]

Mathlib/Order/Hom/Basic.lean

@@ -884,6 +884,13 @@ def prodComm : α × β ≃o β × α where
   toEquiv := Equiv.prodComm α β
   map_rel_iff' := Prod.swap_le_swap
 
+/-- `Equiv.prodAssoc` promoted to an order isomorphism. -/
+@[simps! (attr := grind =)]
+def prodAssoc (α β γ : Type*) [LE α] [LE β] [LE γ] :
+    (α × β) × γ ≃o α × (β × γ) where
+  toEquiv := .prodAssoc α β γ
+  map_rel_iff' := @fun ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ ↦ by simp [Equiv.prodAssoc, and_assoc]
+
 @[simp]
 theorem coe_prodComm : ⇑(prodComm : α × β ≃o β × α) = Prod.swap :=
   rfl
@@ -1069,6 +1076,10 @@ noncomputable def ofUnique
   toEquiv := Equiv.ofUnique α β
   map_rel_iff' := by simp
 
+/-- `Equiv.equivOfIsEmpty` promoted to an `OrderIso`. -/
+def ofIsEmpty (α β : Type*) [Preorder α] [Preorder β] [IsEmpty α] [IsEmpty β] : α ≃o β :=
+  ⟨Equiv.equivOfIsEmpty α β, @isEmptyElim _ _ _⟩
+
 end OrderIso
 
 namespace Equiv

Mathlib/Order/Hom/Lex.lean

@@ -179,4 +179,28 @@ variable {α β} in
 theorem uniqueProd_apply [Preorder α] [Unique α] [LE β] (x : α ×ₗ β) :
     uniqueProd α β x = (ofLex x).2 := rfl
 
+/-- `Equiv.prodAssoc` promoted to an order isomorphism of lexicographic products. -/
+def prodAssoc (α β γ : Type*)
+    [LinearOrder α] [LinearOrder β] [LinearOrder γ] : (α ×ₗ β) ×ₗ γ ≃o α ×ₗ β ×ₗ γ :=
+  { toEquiv := .trans ofLex <| .trans (.prodCongr ofLex <| .refl _) <|
+      .trans (.prodAssoc α β γ) <| .trans (.prodCongr (.refl _) toLex) <| toLex
+    map_rel_iff' := by
+      simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
+      Equiv.prodAssoc_apply]; grind [EmbeddingLike.apply_eq_iff_eq, ofLex_toLex]
+   }
+
+/-- `Equiv.sumProdDistrib` promoted to an order isomorphism of lexicographic products. -/
+def sumProdDistrib (α β γ : Type*)
+    [LinearOrder α] [LinearOrder β] [LinearOrder γ] : (α ⊕ₗ β) ×ₗ γ ≃o α ×ₗ γ ⊕ₗ β ×ₗ γ where
+  toEquiv := .trans ofLex <| .trans (.prodCongr ofLex <| .refl _) <|
+    .trans (.sumProdDistrib α β γ) <| .trans (.sumCongr toLex toLex) toLex
+  map_rel_iff' := by simp [Prod.Lex.le_iff]
+
+/-- `Equiv.prodCongr` promoted to an order isomorphism between lexicographic products. -/
+@[simps! apply]
+def prodCongr {α β γ δ : Type*} [LinearOrder α] [LinearOrder β]
+    [LinearOrder γ] [LinearOrder δ] (ea : α ≃o β) (eb : γ ≃o δ) : α ×ₗ γ ≃o β ×ₗ δ where
+  toEquiv := ofLex.trans ((Equiv.prodCongr ea eb).trans toLex)
+  map_rel_iff' := by simp [Prod.Lex.le_iff]
+
 end Prod.Lex