feat: generalize LE, LT and the Std order-predicate classes to Sort u

src/Init/Data/List/MinMaxIdx.lean

@@ -662,7 +662,7 @@ protected theorem minIdxOn?_eq_ite
   cases xs <;> simp [List.minIdxOn?_cons_eq_some_minIdxOn]
 
 @[deprecated List.minIdxOn?_eq_ite (since := "2026-07-21")]
-protected theorem minIdxOn?_eq_if {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : List.minIdxOn? f xs = if h : xs ≠ [] then Option.some (List.minIdxOn f xs h) else Option.none := List.minIdxOn?_eq_ite
+protected theorem minIdxOn?_eq_if {β : Sort u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : List.minIdxOn? f xs = if h : xs ≠ [] then Option.some (List.minIdxOn f xs h) else Option.none := List.minIdxOn?_eq_ite
 
 protected theorem minIdxOn?_cons
     [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} :
@@ -784,7 +784,7 @@ protected theorem maxIdxOn?_eq_ite
   exact List.minIdxOn?_eq_ite
 
 @[deprecated List.maxIdxOn?_eq_ite (since := "2026-07-21")]
-protected theorem maxIdxOn?_eq_if {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : List.maxIdxOn? f xs = if h : xs ≠ [] then Option.some (List.maxIdxOn f xs h) else Option.none := List.maxIdxOn?_eq_ite
+protected theorem maxIdxOn?_eq_if {β : Sort u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : List.maxIdxOn? f xs = if h : xs ≠ [] then Option.some (List.maxIdxOn f xs h) else Option.none := List.maxIdxOn?_eq_ite
 
 protected theorem maxIdxOn?_cons
     [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} :

src/Init/Data/List/MinMaxOn.lean

@@ -502,7 +502,7 @@ protected theorem minOn?_eq_ite
   fun_cases xs.minOn? f <;> simp [List.minOn]
 
 @[deprecated List.minOn?_eq_ite (since := "2026-07-21")]
-protected theorem minOn?_eq_if {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} : List.minOn? f xs = if h : xs ≠ [] then Option.some (List.minOn f xs h) else Option.none := List.minOn?_eq_ite
+protected theorem minOn?_eq_if {β : Sort u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} : List.minOn? f xs = if h : xs ≠ [] then Option.some (List.minOn f xs h) else Option.none := List.minOn?_eq_ite
 
 @[simp]
 protected theorem isSome_minOn?_iff [LE β] [DecidableLE β] {f : α → β} {xs : List α} :
@@ -617,7 +617,7 @@ protected theorem maxOn?_eq_ite
   List.minOn?_eq_ite
 
 @[deprecated List.maxOn?_eq_ite (since := "2026-07-21")]
-protected theorem maxOn?_eq_if {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} : List.maxOn? f xs = if h : xs ≠ [] then Option.some (List.maxOn f xs h) else Option.none := List.maxOn?_eq_ite
+protected theorem maxOn?_eq_if {β : Sort u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} : List.maxOn? f xs = if h : xs ≠ [] then Option.some (List.maxOn f xs h) else Option.none := List.maxOn?_eq_ite
 
 @[simp]
 protected theorem isSome_maxOn?_iff [LE β] [DecidableLE β] {f : α → β} {xs : List α} :

src/Init/Data/Order/Classes.lean

@@ -51,7 +51,7 @@ theorem lt_trans {α : Type u} [LE α] [LT α]
 This typeclass states that the order structure on `α`, represented by an `LE α` instance,
 is a preorder. In other words, the less-or-equal relation is reflexive and transitive.
 -/
-public class IsPreorder (α : Type u) [LE α] where
+public class IsPreorder (α : Sort u) [LE α] where
   le_refl : ∀ a : α, a ≤ a
   le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
 
@@ -60,23 +60,23 @@ This typeclass states that the order structure on `α`, represented by an `LE α
 is a partial order.
 In other words, the less-or-equal relation is reflexive, transitive and antisymmetric.
 -/
-public class IsPartialOrder (α : Type u) [LE α] extends IsPreorder α where
+public class IsPartialOrder (α : Sort u) [LE α] extends IsPreorder α where
   le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
 
 /--
 This typeclass states that the order structure on `α`, represented by an `LE α` instance,
 is a linear preorder.
 In other words, the less-or-equal relation is reflexive, transitive and total.
 -/
-public class IsLinearPreorder (α : Type u) [LE α] extends IsPreorder α where
+public class IsLinearPreorder (α : Sort u) [LE α] extends IsPreorder α where
   le_total : ∀ a b : α, a ≤ b ∨ b ≤ a
 
 /--
 This typeclass states that the order structure on `α`, represented by an `LE α` instance,
 is a linear order.
 In other words, the less-or-equal relation is reflexive, transitive, antisymmetric and total.
 -/
-public class IsLinearOrder (α : Type u) [LE α] extends IsPartialOrder α, IsLinearPreorder α
+public class IsLinearOrder (α : Sort u) [LE α] extends IsPartialOrder α, IsLinearPreorder α
 
 section LT
 
@@ -91,7 +91,7 @@ be true simultaneously.
 `LT α` does not uniquely determine the `LE α`: There can be only one compatible order data
 instance that is total, but there can be others that are not total.
 -/
-public class LawfulOrderLT (α : Type u) [LT α] [LE α] where
+public class LawfulOrderLT (α : Sort u) [LT α] [LE α] where
   lt_iff : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a
 
 end LT

src/Init/Data/Order/Lemmas.lean

@@ -71,19 +71,19 @@ public theorem Asymm.total_not {r : α → α → Prop} [i : Asymm r] : Total (
     | .inl hba => .inl <| i.asymm b a hba
     | .inr hba => .inr hba
 
-public instance {α : Type u} [LE α] [IsPartialOrder α] :
+public instance {α : Sort u} [LE α] [IsPartialOrder α] :
     Antisymm (α := α) (· ≤ ·) where
   antisymm := IsPartialOrder.le_antisymm
 
-public instance {α : Type u} [LE α] [IsPreorder α] :
+public instance {α : Sort u} [LE α] [IsPreorder α] :
     Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) where
       trans := IsPreorder.le_trans _ _ _
 
-public instance {α : Type u} [LE α] [IsPreorder α] :
+public instance {α : Sort u} [LE α] [IsPreorder α] :
     Refl (α := α) (· ≤ ·) where
   refl := IsPreorder.le_refl
 
-public instance {α : Type u} [LE α] [IsLinearPreorder α] :
+public instance {α : Sort u} [LE α] [IsLinearPreorder α] :
     Total (α := α) (· ≤ ·) where
   total := IsLinearPreorder.le_total
 
@@ -92,84 +92,84 @@ end AxiomaticInstances
 section LE
 
 @[simp]
-public theorem le_refl {α : Type u} [LE α] [Refl (α := α) (· ≤ ·)] (a : α) : a ≤ a := by
+public theorem le_refl {α : Sort u} [LE α] [Refl (α := α) (· ≤ ·)] (a : α) : a ≤ a := by
   simp [Refl.refl]
 
 public theorem le_of_eq [LE α] [Refl (α := α) (· ≤ ·)] {a b : α} : a = b → a ≤ b :=
   (· ▸ le_refl _)
 
-public theorem le_antisymm {α : Type u} [LE α] [Std.Antisymm (α := α) (· ≤ ·)] {a b : α}
+public theorem le_antisymm {α : Sort u} [LE α] [Std.Antisymm (α := α) (· ≤ ·)] {a b : α}
     (hab : a ≤ b) (hba : b ≤ a) : a = b :=
   Antisymm.antisymm _ _ hab hba
 
-public theorem le_antisymm_iff {α : Type u} [LE α] [Antisymm (α := α) (· ≤ ·)]
+public theorem le_antisymm_iff {α : Sort u} [LE α] [Antisymm (α := α) (· ≤ ·)]
     [Refl (α := α) (· ≤ ·)] {a b : α} : a ≤ b ∧ b ≤ a ↔ a = b :=
   ⟨fun | ⟨hab, hba⟩ => le_antisymm hab hba, by simp +contextual [le_refl]⟩
 
-public theorem le_trans {α : Type u} [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] {a b c : α}
+public theorem le_trans {α : Sort u} [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] {a b c : α}
     (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c :=
   Trans.trans hab hbc
 
-public theorem le_total {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)] {a b : α} :
+public theorem le_total {α : Sort u} [LE α] [Std.Total (α := α) (· ≤ ·)] {a b : α} :
     a ≤ b ∨ b ≤ a :=
   Std.Total.total a b
 
-public theorem le_of_not_ge {α : Type u} [LE α] [Std.Total (α := α) (· ≤ ·)] {a b : α} :
+public theorem le_of_not_ge {α : Sort u} [LE α] [Std.Total (α := α) (· ≤ ·)] {a b : α} :
     ¬ b ≤ a → a ≤ b := Total.rel_of_not_rel_swap
 
 end LE
 
 section LT
 
-public theorem lt_trans {α : Type u} [LT α] [Trans (α := α) (· < ·) (· < ·) (· < ·)] {a b c : α}
+public theorem lt_trans {α : Sort u} [LT α] [Trans (α := α) (· < ·) (· < ·) (· < ·)] {a b c : α}
     (hab : a < b) (hbc : b < c) : a < c :=
   Trans.trans hab hbc
 
-public theorem lt_iff_le_and_not_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} :
+public theorem lt_iff_le_and_not_ge {α : Sort u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} :
     a < b ↔ a ≤ b ∧ ¬ b ≤ a :=
   LawfulOrderLT.lt_iff a b
 
-public theorem not_lt_iff_not_le_or_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α]
+public theorem not_lt_iff_not_le_or_ge {α : Sort u} [LT α] [LE α] [LawfulOrderLT α]
     {a b : α} : ¬ a < b ↔ ¬ a ≤ b ∨ b ≤ a := by
   simp only [lt_iff_le_and_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
 
-public theorem not_le_of_gt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
+public theorem not_le_of_gt {α : Sort u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
     (h : a < b) : ¬ b ≤ a := (lt_iff_le_and_not_ge.1 h).2
 
-public theorem not_lt_of_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
+public theorem not_lt_of_ge {α : Sort u} [LT α] [LE α] [LawfulOrderLT α] {a b : α}
     (h : a ≤ b) : ¬ b < a := imp_not_comm.1 not_le_of_gt h
 
-public instance {α : Type u} {_ : LE α} [LT α] [LawfulOrderLT α]
+public instance {α : Sort u} {_ : LE α} [LT α] [LawfulOrderLT α]
     [Trichotomous (α := α) (· < ·)] : Antisymm (α := α) (· ≤ ·) where
   antisymm _ _ hab hba := Trichotomous.trichotomous _ _ (not_lt_of_ge hba) (not_lt_of_ge hab)
 
-public theorem not_gt_of_lt {α : Type u} [LT α] [i : Std.Asymm (α := α) (· < ·)] {a b : α}
+public theorem not_gt_of_lt {α : Sort u} [LT α] [i : Std.Asymm (α := α) (· < ·)] {a b : α}
     (h : a < b) : ¬ b < a :=
   i.asymm a b h
 
-public theorem lt_irrefl {α : Type u} [LT α] [i : Std.Irrefl (α := α) (· < ·)] {a : α} :
+public theorem lt_irrefl {α : Sort u} [LT α] [i : Std.Irrefl (α := α) (· < ·)] {a : α} :
     ¬ a < a :=
   i.irrefl a
 
-public theorem le_of_lt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} (h : a < b) :
+public theorem le_of_lt {α : Sort u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} (h : a < b) :
     a ≤ b := (lt_iff_le_and_not_ge.1 h).1
 
-public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
+public instance {α : Sort u} {_ : LT α} [LE α] [LawfulOrderLT α]
     [Antisymm (α := α) (· ≤ ·)] : Antisymm (α := α) (· < ·) where
   antisymm _ _ hab hba := Antisymm.antisymm _ _ (le_of_lt hab) (le_of_lt hba)
 
-public instance {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :
+public instance {α : Sort u} [LT α] [LE α] [LawfulOrderLT α] :
     Std.Asymm (α := α) (· < ·) where
   asymm a b := by
     simp only [LawfulOrderLT.lt_iff]
     intro h h'
     exact h.2.elim h'.1
 
 @[deprecated instIrreflOfAsymm +typeChanged (since := "2025-10-24")]
-public theorem instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α]
+public theorem instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Sort u} [LT α] [LE α]
     [LawfulOrderLT α] : Std.Irrefl (α := α) (· < ·) := inferInstance
 
-public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]
+public instance {α : Sort u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) ]
     [LawfulOrderLT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where
   trans {a b c} hab hbc := by
     simp only [lt_iff_le_and_not_ge] at hab hbc ⊢
@@ -178,34 +178,34 @@ public instance {α : Type u} [LT α] [LE α] [Trans (α := α) (· ≤ ·) (·
     · intro hca
       exact hab.2.elim (le_trans hbc.1 hca)
 
-public theorem not_lt {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
+public theorem not_lt {α : Sort u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
     {a b : α} : ¬ a < b ↔ b ≤ a := by
   simp [not_lt_iff_not_le_or_ge]
   exact le_of_not_ge
 
-public theorem not_le {α : Type u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
+public theorem not_le {α : Sort u} [LT α] [LE α] [Std.Total (α := α) (· ≤ ·)] [LawfulOrderLT α]
     {a b : α} : ¬ a ≤ b ↔ b < a := by
   simp [lt_iff_le_and_not_ge]
   exact le_of_not_ge
 
-public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
+public instance {α : Sort u} {_ : LT α} [LE α] [LawfulOrderLT α]
     [Total (α := α) (· ≤ ·)] [Antisymm (α := α) (· ≤ ·)] : Trichotomous (α := α) (· < ·) where
   trichotomous a b hab hba := by
     simp only [not_lt] at hab hba
     exact Antisymm.antisymm (r := (· ≤ ·)) a b hba hab
 
-public instance {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
+public instance {α : Sort u} {_ : LT α} [LE α] [LawfulOrderLT α]
     [Total (α := α) (· ≤ ·)] [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] :
     Trans (α := α) (¬ · < ·) (¬ · < ·) (¬ · < ·) where
   trans {a b c} hab hbc := by
     simp only [not_lt] at hab hbc ⊢
     exact le_trans hbc hab
 
 @[deprecated Asymm.total_not +typeChanged (since := "2025-10-24")]
-public theorem instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {_ : LT α} [LE α] [LawfulOrderLT α]
+public theorem instTotalNotLtOfLawfulOrderLTOfLe {α : Sort u} {_ : LT α} [LE α] [LawfulOrderLT α]
     : Total (α := α) (¬ · < ·) := Asymm.total_not
 
-public theorem lt_of_le_of_lt {α : Type u} [LE α] [LT α]
+public theorem lt_of_le_of_lt {α : Sort u} [LE α] [LT α]
     [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] [LawfulOrderLT α] {a b c : α} (hab : a ≤ b)
     (hbc : b < c) : a < c := by
   simp only [lt_iff_le_and_not_ge] at hbc ⊢
@@ -214,7 +214,7 @@ public theorem lt_of_le_of_lt {α : Type u} [LE α] [LT α]
   · intro hca
     exact hbc.2.elim (le_trans hca hab)
 
-public theorem lt_of_lt_of_le {α : Type u} [LE α] [LT α]
+public theorem lt_of_lt_of_le {α : Sort u} [LE α] [LT α]
     [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)] [LawfulOrderLT α] {a b c : α} (hab : a < b)
     (hbc : b ≤ c) : a < c := by
   simp only [lt_iff_le_and_not_ge] at hab ⊢
@@ -223,15 +223,15 @@ public theorem lt_of_lt_of_le {α : Type u} [LE α] [LT α]
   · intro hca
     exact hab.2.elim (le_trans hbc hca)
 
-public theorem lt_of_le_of_ne {α : Type u} [LE α] [LT α]
+public theorem lt_of_le_of_ne {α : Sort u} [LE α] [LT α]
     [Std.Antisymm (α := α) (· ≤ ·)] [LawfulOrderLT α] {a b : α}
     (hle : a ≤ b) (hne : a ≠ b) : a < b := by
   apply Classical.byContradiction
   simp only [lt_iff_le_and_not_ge, hle, true_and, Classical.not_not, imp_false]
   intro hge
   exact hne.elim <| Std.Antisymm.antisymm a b hle hge
 
-public theorem ne_of_lt {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a b : α} : a < b → a ≠ b :=
+public theorem ne_of_lt {α : Sort u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a b : α} : a < b → a ≠ b :=
   fun h h' => absurd (h' ▸ h) (h' ▸ lt_irrefl)
 
 public theorem le_iff_lt_or_eq [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] {a b : α} :
@@ -253,11 +253,11 @@ end Std
 namespace Classical.Order
 open Std
 
-public scoped instance instLT {α : Type u} [LE α] :
+public scoped instance instLT {α : Sort u} [LE α] :
     LT α where
   lt a b := a ≤ b ∧ ¬ b ≤ a
 
-public instance instLawfulOrderLT {α : Type u} [LE α] :
+public instance instLawfulOrderLT {α : Sort u} [LE α] :
     LawfulOrderLT α where
   lt_iff _ _ := Iff.rfl
 

src/Init/Data/Order/MinMaxOn.lean

@@ -129,7 +129,7 @@ public theorem minOn_eq_ite [LE β] [DecidableLE β] {f : α → β} {a b : α}
   (rfl)
 
 @[deprecated minOn_eq_ite (since := "2026-07-21")]
-public theorem minOn_eq_if {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a : α} {b : α} : minOn f a b = if f a ≤ f b then a else b := minOn_eq_ite
+public theorem minOn_eq_if {β : Sort u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a : α} {b : α} : minOn f a b = if f a ≤ f b then a else b := minOn_eq_ite
 
 public theorem minOn_eq_min [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMin α] [LE β]
     [DecidableLE β] {f : α → β} {a b : α} (hf : f a ≤ f b ↔ a ≤ b) :
@@ -219,7 +219,7 @@ public theorem maxOn_eq_ite [LE β] [DecidableLE β] {f : α → β} {a b : α}
   simp only [maxOn_eq_minOn, minOn_eq_ite, LE.le_opposite_iff]
 
 @[deprecated maxOn_eq_ite (since := "2026-07-21")]
-public theorem maxOn_eq_if {β : Type u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a : α} {b : α} : maxOn f a b = if f b ≤ f a then a else b := maxOn_eq_ite
+public theorem maxOn_eq_if {β : Sort u_1} {α : Sort u_2} [LE β] [DecidableLE β] {f : α → β} {a : α} {b : α} : maxOn f a b = if f b ≤ f a then a else b := maxOn_eq_ite
 
 public theorem maxOn_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α] [LE β]
     [DecidableLE β] {f : α → β} {a b : α} (hf : f b ≤ f a ↔ b ≤ a) :

src/Init/Grind/Ordered/Order.lean

@@ -18,7 +18,7 @@ namespace Lean.Grind
 
 namespace Preorder
 
-variable {α : Type u} [LE α] [LT α] [LawfulOrderLT α]
+variable {α : Sort u} [LE α] [LT α] [LawfulOrderLT α]
 
 theorem le_of_lt {a b : α} (h : a < b) : a ≤ b := (lt_iff_le_and_not_ge.mp h).1
 
@@ -55,7 +55,7 @@ end Preorder
 
 namespace PartialOrder
 
-variable {α : Type u} [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α]
+variable {α : Sort u} [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α]
 
 theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by
   constructor
@@ -71,7 +71,7 @@ end PartialOrder
 
 namespace LinearOrder
 
-variable {α : Type u} [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
+variable {α : Sort u} [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
 
 theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by
   cases le_total (a := a) (b := b) with

src/Init/Prelude.lean

@@ -1270,24 +1270,24 @@ instance instOfNatNat (n : Nat) : OfNat Nat n where
   ofNat := n
 
 /-- `LE α` is the typeclass which supports the notation `x ≤ y` where `x y : α`.-/
-class LE (α : Type u) where
+class LE (α : Sort u) where
   /-- The less-equal relation: `x ≤ y` -/
   le : α → α → Prop
 
 /-- `LT α` is the typeclass which supports the notation `x < y` where `x y : α`.-/
-class LT (α : Type u) where
+class LT (α : Sort u) where
   /-- The less-than relation: `x < y` -/
   lt : α → α → Prop
 
 /-- `a ≥ b` is an abbreviation for `b ≤ a`. -/
-@[reducible] def GE.ge {α : Type u} [LE α] (a b : α) : Prop := LE.le b a
+@[reducible] def GE.ge {α : Sort u} [LE α] (a b : α) : Prop := LE.le b a
 /-- `a > b` is an abbreviation for `b < a`. -/
-@[reducible] def GT.gt {α : Type u} [LT α] (a b : α) : Prop := LT.lt b a
+@[reducible] def GT.gt {α : Sort u} [LT α] (a b : α) : Prop := LT.lt b a
 
 /-- Abbreviation for `DecidableRel (· < · : α → α → Prop)`. -/
-abbrev DecidableLT (α : Type u) [LT α] := DecidableRel (LT.lt : α → α → Prop)
+abbrev DecidableLT (α : Sort u) [LT α] := DecidableRel (LT.lt : α → α → Prop)
 /-- Abbreviation for `DecidableRel (· ≤ · : α → α → Prop)`. -/
-abbrev DecidableLE (α : Type u) [LE α] := DecidableRel (LE.le : α → α → Prop)
+abbrev DecidableLE (α : Sort u) [LE α] := DecidableRel (LE.le : α → α → Prop)
 
 /--
 An overloaded operation to find the greater of two values of type `α`.

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -434,9 +434,9 @@ instance : ToFormat GuessLexRel where
 
 /-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/
 def GuessLexRel.toNatRel : GuessLexRel → Expr
-  | lt => mkAppN (mkConst ``LT.lt [Level.zero]) #[mkConst ``Nat, mkConst ``instLTNat]
+  | lt => mkAppN (mkConst ``LT.lt [1]) #[mkConst ``Nat, mkConst ``instLTNat]
   | eq => mkAppN (mkConst ``Eq [Level.one]) #[mkConst ``Nat]
-  | le => mkAppN (mkConst ``LE.le [Level.zero]) #[mkConst ``Nat, mkConst ``instLENat]
+  | le => mkAppN (mkConst ``LE.le [1]) #[mkConst ``Nat, mkConst ``instLENat]
   | no_idea => unreachable!
 
 /--