chore (Data.Nat.Cast.Order): split into Basic and Ring (#14371)

We split `Data.Nat.Cast.Order` into `Data.Nat.Cast.Order.Basic` which only uses unbundled ordered algebra classes and `Data.Nat.Cast.Order.Ring` which uses bundled ordered algebra classes. This avoids importing bundled ordered algebra until later downstream.



Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

Author: mattrobball

Mathlib.lean

@@ -2181,7 +2181,8 @@ 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.Order.Basic
+import Mathlib.Data.Nat.Cast.Order.Ring
 import Mathlib.Data.Nat.Cast.Prod
 import Mathlib.Data.Nat.Cast.SetInterval
 import Mathlib.Data.Nat.Cast.Synonym

Mathlib/Algebra/Order/Group/Nat.lean

@@ -47,8 +47,6 @@ instance instOrderedSub : OrderedSub ℕ := by
 
 /-! ### Miscellaneous lemmas -/
 
-theorem _root_.NeZero.one_le {n : ℕ} [NeZero n] : 1 ≤ n := one_le_iff_ne_zero.mpr (NeZero.ne n)
-
 variable {α : Type*} {n : ℕ} {f : α → ℕ}
 
 /-- See also `pow_left_strictMonoOn`. -/

Mathlib/Algebra/Order/Invertible.lean

@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Ring.Invertible
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Ring
 
 #align_import algebra.order.invertible from "leanprover-community/mathlib"@"ee0c179cd3c8a45aa5bffbf1b41d8dbede452865"
 

Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.Ring.InjSurj
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Ring
 import Mathlib.Order.CompleteLatticeIntervals
 import Mathlib.Order.LatticeIntervals
 

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Algebra.Ring.Divisibility.Basic
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Ring
 
 #align_import algebra.order.ring.abs from "leanprover-community/mathlib"@"10b4e499f43088dd3bb7b5796184ad5216648ab1"
 #align_import data.nat.parity from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"

Mathlib/Algebra/Order/Ring/Cast.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Order.Ring.Int
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Ring
 
 #align_import data.int.cast.lemmas from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
 

Mathlib/Algebra/Order/Ring/Pow.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Data.Nat.Cast.Commute
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Ring
 
 /-! # Bernoulli's inequality -/
 

Mathlib/Data/Nat/Cast/Field.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yaël Dillies, Patrick Stevens
 -/
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Tactic.Common
 
 #align_import data.nat.cast.field from "leanprover-community/mathlib"@"acee671f47b8e7972a1eb6f4eed74b4b3abce829"

Mathlib/Data/Nat/Cast/NeZero.lean

@@ -10,8 +10,12 @@ import Mathlib.Algebra.NeZero
 # Lemmas about nonzero elements of an `AddMonoidWithOne`
 -/
 
+open Nat
+
 namespace NeZero
 
+theorem one_le {n : ℕ} [NeZero n] : 1 ≤ n := by have := NeZero.ne n; omega
+
 lemma natCast_ne (n : ℕ) (R) [AddMonoidWithOne R] [h : NeZero (n : R)] : (n : R) ≠ 0 := h.out
 #align ne_zero.nat_cast_ne NeZero.natCast_ne
 

Mathlib/Data/Nat/Cast/Order.lean renamed to Mathlib/Data/Nat/Cast/Order/Basic.lean

@@ -5,9 +5,10 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Algebra.CharZero.Defs
-import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
 import Mathlib.Data.Nat.Cast.NeZero
-import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Algebra.Order.ZeroLEOne
+import Mathlib.Order.Hom.Basic
 
 #align_import data.nat.cast.basic from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
 
@@ -16,6 +17,8 @@ import Mathlib.Algebra.Order.Ring.Nat
 
 -/
 
+assert_not_exists OrderedCommMonoid
+
 variable {α β : Type*}
 
 namespace Nat
@@ -45,34 +48,11 @@ theorem _root_.GCongr.natCast_le_natCast {a b : ℕ} (h : a ≤ b) : (a : α) 
 theorem cast_nonneg' (n : ℕ) : 0 ≤ (n : α) :=
   @Nat.cast_zero α _ ▸ mono_cast (Nat.zero_le n)
 
-/-- Specialisation of `Nat.cast_nonneg'`, which seems to be easier for Lean to use. -/
-@[simp]
-theorem cast_nonneg {α} [OrderedSemiring α] (n : ℕ) : 0 ≤ (n : α) :=
-  cast_nonneg' n
-#align nat.cast_nonneg Nat.cast_nonneg
-
 /-- See also `Nat.ofNat_nonneg`, specialised for an `OrderedSemiring`. -/
 -- See note [no_index around OfNat.ofNat]
 @[simp low]
 theorem ofNat_nonneg' (n : ℕ) [n.AtLeastTwo] : 0 ≤ (no_index (OfNat.ofNat n : α)) := cast_nonneg' n
 
-/-- Specialisation of `Nat.ofNat_nonneg'`, which seems to be easier for Lean to use. -/
--- See note [no_index around OfNat.ofNat]
-@[simp]
-theorem ofNat_nonneg {α} [OrderedSemiring α] (n : ℕ) [n.AtLeastTwo] :
-    0 ≤ (no_index (OfNat.ofNat n : α)) :=
-  ofNat_nonneg' n
-
-@[simp, norm_cast]
-theorem cast_min {α} [LinearOrderedSemiring α] {a b : ℕ} : ((min a b : ℕ) : α) = min (a : α) b :=
-  (@mono_cast α _).map_min
-#align nat.cast_min Nat.cast_min
-
-@[simp, norm_cast]
-theorem cast_max {α} [LinearOrderedSemiring α] {a b : ℕ} : ((max a b : ℕ) : α) = max (a : α) b :=
-  (@mono_cast α _).map_max
-#align nat.cast_max Nat.cast_max
-
 section Nontrivial
 
 variable [NeZero (1 : α)]
@@ -87,24 +67,6 @@ theorem cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1 := by
 @[simp low]
 theorem cast_pos' {n : ℕ} : (0 : α) < n ↔ 0 < n := by cases n <;> simp [cast_add_one_pos]
 
-/-- Specialisation of `Nat.cast_pos'`, which seems to be easier for Lean to use. -/
-@[simp]
-theorem cast_pos {α} [OrderedSemiring α] [Nontrivial α] {n : ℕ} : (0 : α) < n ↔ 0 < n := cast_pos'
-#align nat.cast_pos Nat.cast_pos
-
-/-- See also `Nat.ofNat_pos`, specialised for an `OrderedSemiring`. -/
--- See note [no_index around OfNat.ofNat]
-@[simp low]
-theorem ofNat_pos' {n : ℕ} [n.AtLeastTwo] : 0 < (no_index (OfNat.ofNat n : α)) :=
-  cast_pos'.mpr (NeZero.pos n)
-
-/-- Specialisation of `Nat.ofNat_pos'`, which seems to be easier for Lean to use. -/
--- See note [no_index around OfNat.ofNat]
-@[simp]
-theorem ofNat_pos {α} [OrderedSemiring α] [Nontrivial α] {n : ℕ} [n.AtLeastTwo] :
-    0 < (no_index (OfNat.ofNat n : α)) :=
-  ofNat_pos'
-
 end Nontrivial
 
 variable [CharZero α] {m n : ℕ}
@@ -140,7 +102,7 @@ theorem one_le_cast : 1 ≤ (n : α) ↔ 1 ≤ n := by rw [← cast_one, cast_le
 
 @[simp, norm_cast]
 theorem cast_lt_one : (n : α) < 1 ↔ n = 0 := by
-  rw [← cast_one, cast_lt, Nat.lt_succ_iff, ← bot_eq_zero, le_bot_iff]
+  rw [← cast_one, cast_lt, Nat.lt_succ_iff, le_zero]
 #align nat.cast_lt_one Nat.cast_lt_one
 
 @[simp, norm_cast]
@@ -149,7 +111,6 @@ theorem cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1 := by rw [← cast_one, cast_le
 
 variable [m.AtLeastTwo] [n.AtLeastTwo]
 
-
 -- TODO: These lemmas need to be `@[simp]` for confluence in the presence of `cast_lt`, `cast_le`,
 -- and `Nat.cast_ofNat`, but their LHSs match literally every inequality, so they're too expensive.
 -- If lean4#2867 is fixed in a performant way, these can be made `@[simp]`.
@@ -210,29 +171,6 @@ theorem not_ofNat_lt_one : ¬(no_index (OfNat.ofNat n : α)) < 1 :=
 
 end OrderedSemiring
 
-/-- A version of `Nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
-for `ℕ∞` and `ℝ≥0∞`, so we use type-specific lemmas for these types. -/
-@[simp, norm_cast]
-theorem cast_tsub [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α]
-    [ContravariantClass α α (· + ·) (· ≤ ·)] (m n : ℕ) : ↑(m - n) = (m - n : α) := by
-  rcases le_total m n with h | h
-  · rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
-    exact mono_cast h
-  · rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
-    rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
-#align nat.cast_tsub Nat.cast_tsub
-
-@[simp, norm_cast]
-theorem abs_cast [LinearOrderedRing α] (a : ℕ) : |(a : α)| = a :=
-  abs_of_nonneg (cast_nonneg a)
-#align nat.abs_cast Nat.abs_cast
-
--- See note [no_index around OfNat.ofNat]
-@[simp]
-theorem abs_ofNat [LinearOrderedRing α] (n : ℕ) [n.AtLeastTwo] :
-    |(no_index (OfNat.ofNat n : α))| = OfNat.ofNat n :=
-  abs_cast n
-
 end Nat
 
 instance [AddMonoidWithOne α] [CharZero α] : Nontrivial α where exists_pair_ne :=