From af1911940422ded96480cde9daed0a5de7a435d3 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Fri, 22 Nov 2024 08:14:07 +0000
Subject: [PATCH] chore: add shortcut instances after LinearOrder Nat (#19346)

This prevents Lean from going through the Lattice structure, which requires additional imports.
---
 Mathlib/Algebra/Prime/Lemmas.lean              | 2 +-
 Mathlib/CategoryTheory/Functor/OfSequence.lean | 1 -
 Mathlib/Data/Int/GCD.lean                      | 2 +-
 Mathlib/Data/Nat/Defs.lean                     | 7 +++++++
 Mathlib/Data/Nat/Log.lean                      | 6 +++---
 Mathlib/Data/Nat/Prime/Defs.lean               | 2 +-
 Mathlib/Data/Nat/Size.lean                     | 1 -
 7 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/Prime/Lemmas.lean b/Mathlib/Algebra/Prime/Lemmas.lean
index 96ee461f3831f..0211c3bbc8c5e 100644
--- a/Mathlib/Algebra/Prime/Lemmas.lean
+++ b/Mathlib/Algebra/Prime/Lemmas.lean
@@ -8,7 +8,7 @@ import Mathlib.Algebra.Group.Even
 import Mathlib.Algebra.Group.Units.Equiv
 import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.Prime.Defs
-import Mathlib.Order.Lattice
+import Mathlib.Order.Monotone.Basic
 
 /-!
 # Associated, prime, and irreducible elements.
diff --git a/Mathlib/CategoryTheory/Functor/OfSequence.lean b/Mathlib/CategoryTheory/Functor/OfSequence.lean
index ba70972cf1661..c1f5788cec33b 100644
--- a/Mathlib/CategoryTheory/Functor/OfSequence.lean
+++ b/Mathlib/CategoryTheory/Functor/OfSequence.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.EqToHom
 
diff --git a/Mathlib/Data/Int/GCD.lean b/Mathlib/Data/Int/GCD.lean
index eccc02d840c40..e6b7b6ec9f4e8 100644
--- a/Mathlib/Data/Int/GCD.lean
+++ b/Mathlib/Data/Int/GCD.lean
@@ -7,8 +7,8 @@ import Mathlib.Algebra.Group.Int
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.Group.Commute.Units
 import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Order.Lattice
 import Mathlib.Data.Set.Operations
+import Mathlib.Order.Basic
 import Mathlib.Order.Bounds.Defs
 
 /-!
diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
index 9063d971434ff..2327e2c3bb37a 100644
--- a/Mathlib/Data/Nat/Defs.lean
+++ b/Mathlib/Data/Nat/Defs.lean
@@ -72,6 +72,13 @@ instance instLinearOrder : LinearOrder ℕ where
   decidableLE := inferInstance
   decidableEq := inferInstance
 
+-- Shortcut instances
+instance : Preorder ℕ := inferInstance
+instance : PartialOrder ℕ := inferInstance
+instance : Min ℕ := inferInstance
+instance : Max ℕ := inferInstance
+instance : Ord ℕ := inferInstance
+
 instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩
 
 @[simp] theorem default_eq_zero : default = 0 := rfl
diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean
index fc11e395a0c41..1d16748dda19e 100644
--- a/Mathlib/Data/Nat/Log.lean
+++ b/Mathlib/Data/Nat/Log.lean
@@ -3,11 +3,11 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yaël Dillies
 -/
+import Mathlib.Order.Interval.Set.Defs
+import Mathlib.Order.Monotone.Basic
 import Mathlib.Tactic.Bound.Attribute
-import Mathlib.Tactic.Monotonicity.Attr
-import Mathlib.Order.Lattice
 import Mathlib.Tactic.Contrapose
-import Mathlib.Order.Interval.Set.Defs
+import Mathlib.Tactic.Monotonicity.Attr
 
 /-!
 # Natural number logarithms
diff --git a/Mathlib/Data/Nat/Prime/Defs.lean b/Mathlib/Data/Nat/Prime/Defs.lean
index 30b5a96a46888..c978c30544721 100644
--- a/Mathlib/Data/Nat/Prime/Defs.lean
+++ b/Mathlib/Data/Nat/Prime/Defs.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 import Batteries.Data.Nat.Gcd
 import Mathlib.Algebra.Prime.Defs
 import Mathlib.Algebra.Ring.Nat
-import Mathlib.Order.Lattice
+import Mathlib.Order.Basic
 
 /-!
 # Prime numbers
diff --git a/Mathlib/Data/Nat/Size.lean b/Mathlib/Data/Nat/Size.lean
index fec3892450d06..fd9311b427815 100644
--- a/Mathlib/Data/Nat/Size.lean
+++ b/Mathlib/Data/Nat/Size.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Data.Nat.Bits
-import Mathlib.Order.Lattice
 
 /-! Lemmas about `size`. -/