diff --git a/Mathlib.lean b/Mathlib.lean
index 39cf4114eae10c..492bbf33062847 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1612,9 +1612,11 @@ import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Data.Nat.Cast.Commute
 import Mathlib.Data.Nat.Cast.Defs
 import Mathlib.Data.Nat.Cast.Field
 import Mathlib.Data.Nat.Cast.NeZero
+import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Data.Nat.Cast.Prod
 import Mathlib.Data.Nat.Cast.WithTop
 import Mathlib.Data.Nat.Choose.Basic
diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean
index 52ccafb303a89f..6b817d450a51f9 100644
--- a/Mathlib/Algebra/GroupPower/Lemmas.lean
+++ b/Mathlib/Algebra/GroupPower/Lemmas.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Data.Nat.Pow
 import Mathlib.Data.Int.Cast.Lemmas
+import Mathlib.Algebra.Group.Opposite
 
 #align_import algebra.group_power.lemmas from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c"
 
diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean
index 076a9e183e524f..6e4e9453701a8e 100644
--- a/Mathlib/Data/Int/Cast/Lemmas.lean
+++ b/Mathlib/Data/Int/Cast/Lemmas.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.Order.Basic
-import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Data.Nat.Cast.Commute
+import Mathlib.Data.Nat.Cast.Order
 
 #align_import data.int.cast.lemmas from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
 
diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean
index 8a8f6636822ccc..a128c9301770f5 100644
--- a/Mathlib/Data/Nat/Cast/Basic.lean
+++ b/Mathlib/Data/Nat/Cast/Basic.lean
@@ -3,14 +3,8 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.CharZero.Defs
-import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.Hom.Ring
-import Mathlib.Algebra.Order.Group.Abs
-import Mathlib.Algebra.Ring.Commute
 import Mathlib.Data.Nat.Order.Basic
-import Mathlib.Data.Nat.Cast.NeZero
-import Mathlib.Algebra.Group.Opposite
 
 #align_import data.nat.cast.basic from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
 
@@ -62,28 +56,6 @@ theorem coe_castRingHom [NonAssocSemiring α] : (castRingHom α : ℕ → α) =
   rfl
 #align nat.coe_cast_ring_hom Nat.coe_castRingHom
 
-theorem cast_commute [NonAssocSemiring α] (n : ℕ) (x : α) : Commute (n : α) x := by
-  induction n with
-  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
-  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
-#align nat.cast_commute Nat.cast_commute
-
-theorem _root_.Commute.ofNat_left [NonAssocSemiring α] (n : ℕ) [n.AtLeastTwo] (x : α) :
-    Commute (OfNat.ofNat n) x :=
-  n.cast_commute x
-
-theorem cast_comm [NonAssocSemiring α] (n : ℕ) (x : α) : (n : α) * x = x * n :=
-  (cast_commute n x).eq
-#align nat.cast_comm Nat.cast_comm
-
-theorem commute_cast [NonAssocSemiring α] (x : α) (n : ℕ) : Commute x n :=
-  (n.cast_commute x).symm
-#align nat.commute_cast Nat.commute_cast
-
-theorem _root_.Commute.ofNat_right [NonAssocSemiring α] (x : α) (n : ℕ) [n.AtLeastTwo] :
-    Commute x (OfNat.ofNat n) :=
-  n.commute_cast x
-
 section OrderedSemiring
 /- Note: even though the section indicates `OrderedSemiring`, which is the common use case,
 we use a generic collection of instances so that it applies in other settings (e.g., in a
@@ -126,46 +98,6 @@ theorem cast_pos {α} [OrderedSemiring α] [Nontrivial α] {n : ℕ} : (0 : α)
 
 end Nontrivial
 
-variable [CharZero α] {m n : ℕ}
-
-theorem strictMono_cast : StrictMono (Nat.cast : ℕ → α) :=
-  mono_cast.strictMono_of_injective cast_injective
-#align nat.strict_mono_cast Nat.strictMono_cast
-
-/-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/
-@[simps! (config := { fullyApplied := false })]
-def castOrderEmbedding : ℕ ↪o α :=
-  OrderEmbedding.ofStrictMono Nat.cast Nat.strictMono_cast
-#align nat.cast_order_embedding Nat.castOrderEmbedding
-#align nat.cast_order_embedding_apply Nat.castOrderEmbedding_apply
-
-@[simp, norm_cast]
-theorem cast_le : (m : α) ≤ n ↔ m ≤ n :=
-  strictMono_cast.le_iff_le
-#align nat.cast_le Nat.cast_le
-
-@[simp, norm_cast, mono]
-theorem cast_lt : (m : α) < n ↔ m < n :=
-  strictMono_cast.lt_iff_lt
-#align nat.cast_lt Nat.cast_lt
-
-@[simp, norm_cast]
-theorem one_lt_cast : 1 < (n : α) ↔ 1 < n := by rw [← cast_one, cast_lt]
-#align nat.one_lt_cast Nat.one_lt_cast
-
-@[simp, norm_cast]
-theorem one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n := by rw [← cast_one, cast_le]
-#align nat.one_le_cast Nat.one_le_cast
-
-@[simp, norm_cast]
-theorem cast_lt_one : (n : α) < 1 ↔ n = 0 := by
-  rw [← cast_one, cast_lt, lt_succ_iff, ← bot_eq_zero, le_bot_iff]
-#align nat.cast_lt_one Nat.cast_lt_one
-
-@[simp, norm_cast]
-theorem cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1 := by rw [← cast_one, cast_le]
-#align nat.cast_le_one Nat.cast_le_one
-
 end OrderedSemiring
 
 /-- A version of `Nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
@@ -190,11 +122,6 @@ theorem cast_max [LinearOrderedSemiring α] {a b : ℕ} : ((max a b : ℕ) : α)
   (@mono_cast α _).map_max
 #align nat.cast_max Nat.cast_max
 
-@[simp, norm_cast]
-theorem abs_cast [LinearOrderedRing α] (a : ℕ) : |(a : α)| = a :=
-  abs_of_nonneg (cast_nonneg a)
-#align nat.abs_cast Nat.abs_cast
-
 theorem coe_nat_dvd [Semiring α] {m n : ℕ} (h : m ∣ n) : (m : α) ∣ (n : α) :=
   map_dvd (Nat.castRingHom α) h
 #align nat.coe_nat_dvd Nat.coe_nat_dvd
@@ -203,9 +130,6 @@ alias _root_.Dvd.dvd.natCast := coe_nat_dvd
 
 end Nat
 
-instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α where exists_pair_ne :=
-  ⟨1, 0, (Nat.cast_one (R := α) ▸ Nat.cast_ne_zero.2 (by decide))⟩
-
 section AddMonoidHomClass
 
 variable {A B F : Type*} [AddMonoidWithOne B]
@@ -285,11 +209,6 @@ theorem ext_nat [RingHomClass F ℕ R] (f g : F) : f = g :=
   ext_nat' f g <| by simp only [map_one f, map_one g]
 #align ext_nat ext_nat
 
-theorem NeZero.nat_of_injective {n : ℕ} [h : NeZero (n : R)] [RingHomClass F R S] {f : F}
-    (hf : Function.Injective f) : NeZero (n : S) :=
-  ⟨fun h ↦ NeZero.natCast_ne n R <| hf <| by simpa only [map_natCast, map_zero f] ⟩
-#align ne_zero.nat_of_injective NeZero.nat_of_injective
-
 theorem NeZero.nat_of_neZero {R S} [Semiring R] [Semiring S] {F} [RingHomClass F R S] (f : F)
     {n : ℕ} [hn : NeZero (n : S)] : NeZero (n : R) :=
   .of_map (f := f) (neZero := by simp only [map_natCast, hn])
@@ -394,3 +313,11 @@ theorem toLex_natCast [NatCast α] (n : ℕ) : toLex (n : α) = n :=
 theorem ofLex_natCast [NatCast α] (n : ℕ) : (ofLex n : α) = n :=
   rfl
 #align of_lex_nat_cast ofLex_natCast
+
+-- Guard against import creep regression.
+assert_not_exists CharZero
+assert_not_exists Commute.zero_right
+assert_not_exists Commute.add_right
+assert_not_exists abs_eq_max_neg
+assert_not_exists natCast_ne
+assert_not_exists MulOpposite.natCast
diff --git a/Mathlib/Data/Nat/Cast/Commute.lean b/Mathlib/Data/Nat/Cast/Commute.lean
new file mode 100644
index 00000000000000..48309d0c0b4937
--- /dev/null
+++ b/Mathlib/Data/Nat/Cast/Commute.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2014 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Algebra.GroupWithZero.Commute
+import Mathlib.Algebra.Ring.Commute
+
+#align_import data.nat.cast.basic from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
+
+/-!
+# Cast of natural numbers: lemmas about `Commute`
+
+-/
+
+variable {α β : Type*}
+
+namespace Nat
+
+section Commute
+
+theorem cast_commute [NonAssocSemiring α] (n : ℕ) (x : α) : Commute (n : α) x := by
+  induction n with
+  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
+  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
+#align nat.cast_commute Nat.cast_commute
+
+theorem _root_.Commute.ofNat_left [NonAssocSemiring α] (n : ℕ) [n.AtLeastTwo] (x : α) :
+    Commute (OfNat.ofNat n) x :=
+  n.cast_commute x
+
+theorem cast_comm [NonAssocSemiring α] (n : ℕ) (x : α) : (n : α) * x = x * n :=
+  (cast_commute n x).eq
+#align nat.cast_comm Nat.cast_comm
+
+theorem commute_cast [NonAssocSemiring α] (x : α) (n : ℕ) : Commute x n :=
+  (n.cast_commute x).symm
+#align nat.commute_cast Nat.commute_cast
+
+theorem _root_.Commute.ofNat_right [NonAssocSemiring α] (x : α) (n : ℕ) [n.AtLeastTwo] :
+    Commute x (OfNat.ofNat n) :=
+  n.commute_cast x
+
+end Commute
diff --git a/Mathlib/Data/Nat/Cast/Field.lean b/Mathlib/Data/Nat/Cast/Field.lean
index 3a9c43fb4057f7..eab004e8ad8e10 100644
--- a/Mathlib/Data/Nat/Cast/Field.lean
+++ b/Mathlib/Data/Nat/Cast/Field.lean
@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Yaël Dillies, Patrick Stevens
 -/
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Ring.CharZero
-import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Tactic.Common
 
 #align_import data.nat.cast.field from "leanprover-community/mathlib"@"acee671f47b8e7972a1eb6f4eed74b4b3abce829"
diff --git a/Mathlib/Data/Nat/Cast/Order.lean b/Mathlib/Data/Nat/Cast/Order.lean
new file mode 100644
index 00000000000000..a0ffa93b34cd88
--- /dev/null
+++ b/Mathlib/Data/Nat/Cast/Order.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2014 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Algebra.CharZero.Defs
+import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Data.Nat.Cast.NeZero
+
+#align_import data.nat.cast.basic from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
+
+/-!
+# Cast of natural numbers: lemmas about order
+
+-/
+
+variable {α β : Type*}
+
+namespace Nat
+
+section OrderedSemiring
+/- Note: even though the section indicates `OrderedSemiring`, which is the common use case,
+we use a generic collection of instances so that it applies in other settings (e.g., in a
+`StarOrderedRing`, or the `selfAdjoint` or `StarOrderedRing.positive` parts thereof). -/
+
+variable [AddCommMonoidWithOne α] [PartialOrder α]
+variable [CovariantClass α α (· + ·) (· ≤ ·)] [ZeroLEOneClass α]
+variable [CharZero α] {m n : ℕ}
+
+theorem strictMono_cast : StrictMono (Nat.cast : ℕ → α) :=
+  mono_cast.strictMono_of_injective cast_injective
+#align nat.strict_mono_cast Nat.strictMono_cast
+
+/-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/
+@[simps! (config := { fullyApplied := false })]
+def castOrderEmbedding : ℕ ↪o α :=
+  OrderEmbedding.ofStrictMono Nat.cast Nat.strictMono_cast
+#align nat.cast_order_embedding Nat.castOrderEmbedding
+#align nat.cast_order_embedding_apply Nat.castOrderEmbedding_apply
+
+@[simp, norm_cast]
+theorem cast_le : (m : α) ≤ n ↔ m ≤ n :=
+  strictMono_cast.le_iff_le
+#align nat.cast_le Nat.cast_le
+
+@[simp, norm_cast, mono]
+theorem cast_lt : (m : α) < n ↔ m < n :=
+  strictMono_cast.lt_iff_lt
+#align nat.cast_lt Nat.cast_lt
+
+@[simp, norm_cast]
+theorem one_lt_cast : 1 < (n : α) ↔ 1 < n := by rw [← cast_one, cast_lt]
+#align nat.one_lt_cast Nat.one_lt_cast
+
+@[simp, norm_cast]
+theorem one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n := by rw [← cast_one, cast_le]
+#align nat.one_le_cast Nat.one_le_cast
+
+@[simp, norm_cast]
+theorem cast_lt_one : (n : α) < 1 ↔ n = 0 := by
+  rw [← cast_one, cast_lt, lt_succ_iff, ← bot_eq_zero, le_bot_iff]
+#align nat.cast_lt_one Nat.cast_lt_one
+
+@[simp, norm_cast]
+theorem cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1 := by rw [← cast_one, cast_le]
+#align nat.cast_le_one Nat.cast_le_one
+
+end OrderedSemiring
+
+@[simp, norm_cast]
+theorem abs_cast [LinearOrderedRing α] (a : ℕ) : |(a : α)| = a :=
+  abs_of_nonneg (cast_nonneg a)
+#align nat.abs_cast Nat.abs_cast
+
+end Nat
+
+instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α where exists_pair_ne :=
+  ⟨1, 0, (Nat.cast_one (R := α) ▸ Nat.cast_ne_zero.2 (by decide))⟩
+
+section RingHomClass
+
+variable {R S F : Type*} [NonAssocSemiring R] [NonAssocSemiring S]
+
+theorem NeZero.nat_of_injective {n : ℕ} [h : NeZero (n : R)] [RingHomClass F R S] {f : F}
+    (hf : Function.Injective f) : NeZero (n : S) :=
+  ⟨fun h ↦ NeZero.natCast_ne n R <| hf <| by simpa only [map_natCast, map_zero f] ⟩
+#align ne_zero.nat_of_injective NeZero.nat_of_injective
+
+end RingHomClass
diff --git a/Mathlib/Data/Nat/Choose/Central.lean b/Mathlib/Data/Nat/Choose/Central.lean
index fe6bfa8d1e17b6..796fa79186b091 100644
--- a/Mathlib/Data/Nat/Choose/Central.lean
+++ b/Mathlib/Data/Nat/Choose/Central.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Stevens, Thomas Browning
 -/
 import Mathlib.Data.Nat.Choose.Basic
+import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Linarith
 
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
index a36d92b5f0be7d..30d62314ebea6b 100644
--- a/Mathlib/Data/Rat/Defs.lean
+++ b/Mathlib/Data/Rat/Defs.lean
@@ -5,10 +5,9 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Data.Rat.Init
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Data.Int.Dvd.Basic
-import Mathlib.Algebra.Ring.Regular
-import Mathlib.Data.Nat.GCD.Basic
-import Mathlib.Data.PNat.Defs
+import Mathlib.Data.Int.Order.Basic
+import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Algebra.GroupWithZero.Basic
 
 #align_import data.rat.defs from "leanprover-community/mathlib"@"18a5306c091183ac90884daa9373fa3b178e8607"
 
@@ -84,10 +83,6 @@ lemma num_eq_zero {q : ℚ} : q.num = 0 ↔ q = 0 := by
     exact zero_mk _ _ _
   · exact congr_arg num
 
-private theorem gcd_abs_dvd_left {a b} : (Nat.gcd (Int.natAbs a) b : ℤ) ∣ a :=
-  Int.dvd_natAbs.1 <| Int.coe_nat_dvd.2 <| Nat.gcd_dvd_left (Int.natAbs a) b
--- Porting note: no #align here as the declaration is private.
-
 @[simp]
 theorem divInt_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0 := by
   rw [←zero_divInt b, divInt_eq_iff b0 b0, zero_mul, mul_eq_zero, or_iff_left b0]
@@ -551,7 +546,7 @@ theorem mkRat_eq_div {n : ℤ} {d : ℕ} : mkRat n d = n / d := by
   · simp [h, HDiv.hDiv, Rat.div, Div.div]
     unfold Rat.inv
     have h₁ : 0 < d := Nat.pos_iff_ne_zero.2 h
-    have h₂ : ¬ (d : ℤ) < 0 := by simp
+    have h₂ : ¬ (d : ℤ) < 0 := by simp only [not_lt, Nat.cast_nonneg]
     simp [h, h₁, h₂, ←Rat.normalize_eq_mk', Rat.normalize_eq_mkRat, ← mkRat_one,
       Rat.mkRat_mul_mkRat]
 
@@ -559,3 +554,6 @@ end Rat
 
 -- Guard against import creep.
 assert_not_exists Field
+assert_not_exists PNat
+assert_not_exists Nat.dvd_mul
+assert_not_exists IsDomain.toCancelMonoidWithZero
diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean
index 8557a02de1d4bc..400709ab9248e7 100644
--- a/Mathlib/Data/Rat/Lemmas.lean
+++ b/Mathlib/Data/Rat/Lemmas.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.Data.Int.Div
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Tactic.Replace
+import Mathlib.Data.PNat.Defs
 
 #align_import data.rat.lemmas from "leanprover-community/mathlib"@"550b58538991c8977703fdeb7c9d51a5aa27df11"