From 9b6a4a7588945f6994530616b45272250bb9af71 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 4 Sep 2025 17:27:09 +0200
Subject: [PATCH] fix: solve two problems with `LinearOrderPackage` factories
 (#10250)

This PR fixes a bug in the `LinearOrderPackage.ofOrd` factory. If there
is a `LawfulEqOrd` instance available, it should automatically use it
instead of requiring the user to provide the `eq_of_compare` argument to
the factory. The PR also solves a hygiene-related problem making the
factories fail when `Std` is not open.
---
 src/Init/Data/Order/PackageFactories.lean | 54 +++++++++---------
 tests/lean/run/order.lean                 | 68 ++++++++++++-----------
 2 files changed, 64 insertions(+), 58 deletions(-)

diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean
index f8d0beee98..e0dd05552e 100644
--- a/src/Init/Data/Order/PackageFactories.lean
+++ b/src/Init/Data/Order/PackageFactories.lean
@@ -67,20 +67,20 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact Classical.Order.instLT
+    | exact _root_.Classical.Order.instLT
   beq :
     let := le; let := decidableLE
     BEq α := by
     extract_lets
     first
     | infer_instance
-    | exact FactoryInstances.beqOfDecidableLE
+    | exact _root_.Std.FactoryInstances.beqOfDecidableLE
   lt_iff :
       let := le; let := lt
       ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a := by
     extract_lets
     first
-    | exact LawfulOrderLT.lt_iff
+    | exact _root_.Std.LawfulOrderLT.lt_iff
     | fail "Failed to automatically prove that the `LE` and `LT` instances are compatible. \
             Please ensure that a `LawfulOrderLT` instance can be synthesized or \
             manually provide the field `lt_iff`."
@@ -89,10 +89,10 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       have := lt_iff
       DecidableLT α := by
     extract_lets
-    haveI := @LawfulOrderLT.mk (lt_iff := by assumption) ..
+    haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..
     first
     | infer_instance
-    | exact FactoryInstances.decidableLTOfLE
+    | exact _root_.Std.FactoryInstances.decidableLTOfLE
     | fail "Failed to automatically derive that `LT` is decidable. \
             Please ensure that a `DecidableLT` instance can be synthesized or \
             manually provide the field `decidableLT`."
@@ -101,7 +101,7 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       ∀ a b : α, a == b ↔ a ≤ b ∧ b ≤ a := by
     extract_lets
     first
-      | exact LawfulOrderBEq.beq_iff_le_and_ge
+      | exact _root_.Std.LawfulOrderBEq.beq_iff_le_and_ge
       | fail "Failed to automatically prove that the `LE` and `BEq` instances are compatible. \
               Please ensure that a `LawfulOrderBEq` instance can be synthesized or \
               manually provide the field `beq_iff_le_and_ge`."
@@ -110,7 +110,7 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       ∀ a : α, a ≤ a := by
     extract_lets
     first
-    | exact Std.Refl.refl (r := (· ≤ ·))
+    | exact _root_.Std.Refl.refl (r := (· ≤ ·))
     | fail "Failed to automatically prove that the `LE` instance is reflexive. \
             Please ensure that a `Refl` instance can be synthesized or \
             manually provide the field `le_refl`."
@@ -119,7 +119,7 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c := by
     extract_lets
     first
-    | exact fun _ _ _ hab hbc => Trans.trans (r := (· ≤ ·)) (s := (· ≤ ·)) (t := (· ≤ ·)) hab hbc
+    | exact fun _ _ _ hab hbc => _root_.Trans.trans (r := (· ≤ ·)) (s := (· ≤ ·)) (t := (· ≤ ·)) hab hbc
     | fail "Failed to automatically prove that the `LE` instance is transitive. \
             Please ensure that a `Trans` instance can be synthesized or \
             manually provide the field `le_trans`."
@@ -202,7 +202,7 @@ public structure Packages.PartialOrderOfLEArgs (α : Type u) extends Packages.Pr
       ∀ a b : α, a ≤ b → b ≤ a → a = b := by
     extract_lets
     first
-    | exact Antisymm.antisymm
+    | exact _root_.Std.Antisymm.antisymm
     | fail "Failed to automatically prove that the `LE` instance is antisymmetric. \
             Please ensure that a `Antisymm` instance can be synthesized or \
             manually provide the field `le_antisymm`."
@@ -310,11 +310,11 @@ public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends
     extract_lets
     first
     | infer_instance
-    | exact FactoryInstances.instOrdOfDecidableLE
+    | exact _root_.Std.FactoryInstances.instOrdOfDecidableLE
   le_total :
       ∀ a b : α, a ≤ b ∨ b ≤ a := by
     first
-    | exact Total.total
+    | exact _root_.Std.Total.total
     | fail "Failed to automatically prove that the `LE` instance is total. \
             Please ensure that a `Total` instance can be synthesized or \
             manually provide the field `le_total`."
@@ -324,7 +324,7 @@ public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends
       ∀ a b : α, (compare a b).isLE ↔ a ≤ b := by
     extract_lets
     first
-    | exact LawfulOrderOrd.isLE_compare
+    | exact _root_.Std.LawfulOrderOrd.isLE_compare
     | fail "Failed to automatically prove that `(compare a b).isLE` is equivalent to `a ≤ b`. \
             Please ensure that a `LawfulOrderOrd` instance can be synthesized or \
             manually provide the field `isLE_compare`."
@@ -333,7 +333,7 @@ public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends
       ∀ a b : α, (compare a b).isGE ↔ b ≤ a := by
     extract_lets
     first
-    | exact LawfulOrderOrd.isGE_compare
+    | exact _root_.Std.LawfulOrderOrd.isGE_compare
     | fail "Failed to automatically prove that `(compare a b).isGE` is equivalent to `b ≤ a`. \
             Please ensure that a `LawfulOrderOrd` instance can be synthesized or \
             manually provide the field `isGE_compare`."
@@ -411,20 +411,20 @@ public structure Packages.LinearOrderOfLEArgs (α : Type u) extends
     extract_lets
     first
     | infer_instance
-    | exact Min.leftLeaningOfLE _
+    | exact _root_.Min.leftLeaningOfLE _
   max :
       let := le; let := decidableLE
       Max α := by
     extract_lets
     first
     | infer_instance
-    | exact Max.leftLeaningOfLE _
+    | exact _root_.Max.leftLeaningOfLE _
   min_eq :
       let := le; let := decidableLE; let := min
       ∀ a b : α, Min.min a b = if a ≤ b then a else b := by
     extract_lets
     first
-    | exact fun a b => Std.min_eq_if (a := a) (b := b)
+    | exact fun a b => _root_.Std.min_eq_if (a := a) (b := b)
     | fail "Failed to automatically prove that `min` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \
             manually provide the field `min_eq`."
@@ -433,7 +433,7 @@ public structure Packages.LinearOrderOfLEArgs (α : Type u) extends
       ∀ a b : α, Max.max a b = if b ≤ a then a else b := by
     extract_lets
     first
-    | exact fun a b => Std.max_eq_if (a := a) (b := b)
+    | exact fun a b => _root_.Std.max_eq_if (a := a) (b := b)
     | fail "Failed to automatically prove that `max` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \
             manually provide the field `max_eq`."
@@ -538,7 +538,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact LE.ofOrd _
+    | exact _root_.LE.ofOrd _
   lawfulOrderOrd :
       let := ord; let := transOrd; let := le
       LawfulOrderOrd α := by
@@ -554,7 +554,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact DecidableLE.ofOrd _
+    | exact _root_.DecidableLE.ofOrd _
     | fail "Failed to automatically derive that `LE` is decidable.\
             Please ensure that a `DecidableLE` instance can be synthesized or \
             manually provide the field `decidableLE`."
@@ -570,7 +570,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
       ∀ a b : α, a < b ↔ compare a b = .lt := by
     extract_lets
     first
-    | exact fun _ _ => Std.compare_eq_lt.symm
+    | exact fun _ _ => _root_.Std.compare_eq_lt.symm
     | fail "Failed to automatically derive that `LT` and `Ord` are compatible. \
             Please ensure that a `LawfulOrderLT` instance can be synthesized or \
             manually provide the field `lt_iff`."
@@ -580,7 +580,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact DecidableLT.ofOrd _
+    | exact _root_DecidableLT.ofOrd _
     | fail "Failed to automatically derive that `LT` is decidable. \
             Please ensure that a `DecidableLT` instance can be synthesized or \
             manually provide the field `decidableLT`."
@@ -589,7 +589,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact BEq.ofOrd _
+    | exact _root_.BEq.ofOrd _
   beq_iff :
       let := ord; let := le; have := lawfulOrderOrd; let := beq
       ∀ a b : α, a == b ↔ compare a b = .eq := by
@@ -708,7 +708,7 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
       ∀ a b : α, compare a b = .eq → a = b := by
     extract_lets
     first
-    | exact LawfulEqOrd.eq_of_compare
+    | exact fun _ _ => _root_.Std.LawfulEqOrd.eq_of_compare
     | fail "Failed to derive a `LawfulEqOrd` instance. \
             Please make sure that it can be synthesized or \
             manually provide the field `eq_of_compare`."
@@ -718,20 +718,20 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
     extract_lets
     first
     | infer_instance
-    | exact FactoryInstances.instMinOfOrd
+    | exact _root_.Std.FactoryInstances.instMinOfOrd
   max :
       let := ord
       Max α := by
     extract_lets
     first
     | infer_instance
-    | exact FactoryInstances.instMaxOfOrd
+    | exact _root_.Std.FactoryInstances.instMaxOfOrd
   min_eq :
       let := ord; let := le; let := min; have := lawfulOrderOrd
       ∀ a b : α, Min.min a b = if (compare a b).isLE then a else b := by
     extract_lets
     first
-    | exact fun a b => Std.min_eq_if_isLE_compare (a := a) (b := b)
+    | exact fun a b => _root_.Std.min_eq_if_isLE_compare (a := a) (b := b)
     | fail "Failed to automatically prove that `min` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \
             manually provide the field `min_eq`."
@@ -740,7 +740,7 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
       ∀ a b : α, Max.max a b = if (compare a b).isGE then a else b := by
     extract_lets
     first
-    | exact fun a b => Std.max_eq_if_isGE_compare (a := a) (b := b)
+    | exact fun a b => _root_.Std.max_eq_if_isGE_compare (a := a) (b := b)
     | fail "Failed to automatically prove that `max` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \
             manually provide the field `max_eq`."
diff --git a/tests/lean/run/order.lean b/tests/lean/run/order.lean
index 9035b4a6c5..b023428dae 100644
--- a/tests/lean/run/order.lean
+++ b/tests/lean/run/order.lean
@@ -1,8 +1,6 @@
 
 import Init.Data.Order.PackageFactories
 
-open Std
-
 variable {α : Type u}
 
 opaque X : Type := Unit
@@ -17,44 +15,44 @@ attribute [scoped instance] instLE
 @[scoped instance] opaque instDecidableLE : DecidableLE X := sorry
 
 #guard_msgs(error, drop warning) in
-@[instance] opaque instTotal : Total (α := X) (· ≤ ·) := sorry
+@[instance] opaque instTotal : Std.Total (α := X) (· ≤ ·) := sorry
 
 #guard_msgs(error, drop warning) in
-@[instance] opaque instAntisymm : Antisymm (α := X) (· ≤ ·) := sorry
+@[instance] opaque instAntisymm : Std.Antisymm (α := X) (· ≤ ·) := sorry
 
 #guard_msgs(error, drop warning) in
 @[instance] opaque instTrans : Trans (α := X) (· ≤ ·) (· ≤ ·) (· ≤ ·) := sorry
 
 namespace LinearOrderPackage
 
-scoped instance packageOfLE : LinearOrderPackage X := .ofLE X
+scoped instance packageOfLE : Std.LinearOrderPackage X := .ofLE X
 
-example : instLE = (inferInstanceAs (PreorderPackage X)).toLE := rfl
-example : IsLinearOrder X := inferInstance
-example : LawfulOrderLT X := inferInstance
-example : LawfulOrderOrd X := inferInstance
-example : LawfulOrderMin X := inferInstance
-example : LawfulOrderMax X := inferInstance
-example : LawfulOrderLeftLeaningMin X := inferInstance
-example : LawfulOrderLeftLeaningMax X := inferInstance
+example : instLE = (inferInstanceAs (Std.PreorderPackage X)).toLE := rfl
+example : Std.IsLinearOrder X := inferInstance
+example : Std.LawfulOrderLT X := inferInstance
+example : Std.LawfulOrderOrd X := inferInstance
+example : Std.LawfulOrderMin X := inferInstance
+example : Std.LawfulOrderMax X := inferInstance
+example : Std.LawfulOrderLeftLeaningMin X := inferInstance
+example : Std.LawfulOrderLeftLeaningMax X := inferInstance
 
 end LinearOrderPackage
 
 namespace LinearPreorderPackage
 
-scoped instance packageOfLE : LinearPreorderPackage X := .ofLE X
+scoped instance packageOfLE : Std.LinearPreorderPackage X := .ofLE X
 
 scoped instance instMin : Min X := .leftLeaningOfLE X
 scoped instance instMax : Max X := .leftLeaningOfLE X
 
-example : instLE = (inferInstanceAs (LinearPreorderPackage X)).toLE := rfl
-example : IsLinearPreorder X := inferInstance
-example : LawfulOrderLT X := inferInstance
-example : LawfulOrderOrd X := inferInstance
-example : LawfulOrderMin X := inferInstance
-example : LawfulOrderMax X := inferInstance
-example : LawfulOrderLeftLeaningMin X := inferInstance
-example : LawfulOrderLeftLeaningMax X := inferInstance
+example : instLE = (inferInstanceAs (Std.LinearPreorderPackage X)).toLE := rfl
+example : Std.IsLinearPreorder X := inferInstance
+example : Std.LawfulOrderLT X := inferInstance
+example : Std.LawfulOrderOrd X := inferInstance
+example : Std.LawfulOrderMin X := inferInstance
+example : Std.LawfulOrderMax X := inferInstance
+example : Std.LawfulOrderLeftLeaningMin X := inferInstance
+example : Std.LawfulOrderLeftLeaningMax X := inferInstance
 
 end LinearPreorderPackage
 
@@ -62,7 +60,7 @@ end X
 
 section
 
-def packageWithoutSynthesizableInstances : LinearOrderPackage X := .ofLE X {
+def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofLE X {
   le := X.instLE
   decidableLE := X.instDecidableLE }
 
@@ -72,7 +70,7 @@ section
 
 attribute [local instance] X.LinearOrderPackage.packageOfLE
 
-def packageWithoutSynthesizableInstances' : LinearOrderPackage X := .ofLE X {
+def packageWithoutSynthesizableInstances' : Std.LinearOrderPackage X := .ofLE X {
   le := X.instLE
   decidableLE := X.instDecidableLE
 }
@@ -92,30 +90,30 @@ this✝ : LT α := inferInstance
 ⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
 -/
 #guard_msgs in
-def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : PreorderPackage α := .ofLE α {
+def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : Std.PreorderPackage α := .ofLE α {
   le_refl := sorry
   le_trans := sorry }
 
 def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) :
-    PreorderPackage α := .ofLE α {
+    Std.PreorderPackage α := .ofLE α {
   lt_iff := h
   le_refl := sorry
   le_trans := sorry }
 
 namespace OrdTests
 
-section
+section WithoutSynthesizableInstances
 
 #guard_msgs(error, drop warning) in
 opaque _root_.X.instOrd : Ord X := sorry
 
 #guard_msgs(error, drop warning) in
-opaque _root_.X.instTransOrd : haveI := X.instOrd; TransOrd X := sorry
+opaque _root_.X.instTransOrd : haveI := X.instOrd; Std.TransOrd X := sorry
 
 #guard_msgs(error, drop warning) in
-opaque _root_.X.instLawfulEqOrd : haveI := X.instOrd; LawfulEqOrd X := sorry
+opaque _root_.X.instLawfulEqOrd : haveI := X.instOrd; Std.LawfulEqOrd X := sorry
 
-def packageWithoutSynthesizableInstances : LinearOrderPackage X := .ofOrd X {
+def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X {
   ord := X.instOrd
   transOrd := X.instTransOrd
   eq_of_compare := by
@@ -124,6 +122,14 @@ def packageWithoutSynthesizableInstances : LinearOrderPackage X := .ofOrd X {
     letI := X.instOrd
     exact X.instLawfulEqOrd.eq_of_compare }
 
-end
+end WithoutSynthesizableInstances
+
+section WithSynthesizableInstances
+
+attribute [scoped instance] X.instOrd X.instTransOrd X.instLawfulEqOrd
+
+def packageWithSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X
+
+end WithSynthesizableInstances
 
 end OrdTests