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 <[email protected]>
leanprover-community · Jul 3, 2024 · e66c5a9 · e66c5a9
1 parent 83e2503
commit e66c5a9
Show file tree

Hide file tree

Showing 16 changed files with 130 additions and 82 deletions.
diff --git a/Mathlib.lean b/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

diff --git a/Mathlib/Algebra/Order/Group/Nat.lean b/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`. -/

diff --git a/Mathlib/Algebra/Order/Invertible.lean b/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"
 

diff --git a/Mathlib/Algebra/Order/Nonneg/Ring.lean b/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
 

diff --git a/Mathlib/Algebra/Order/Ring/Abs.lean b/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"

diff --git a/Mathlib/Algebra/Order/Ring/Cast.lean b/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"
 

diff --git a/Mathlib/Algebra/Order/Ring/Pow.lean b/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 -/
 

diff --git a/Mathlib/Data/Nat/Cast/Field.lean b/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"

diff --git a/Mathlib/Data/Nat/Cast/NeZero.lean b/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
 

diff --git a/Mathlib/Data/Nat/Cast/Order.lean → Mathlib/Data/Nat/Cast/Order/Basic.lean b/Mathlib/Data/Nat/Cast/Order.lean → 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 :=

diff --git a/Mathlib/Data/Nat/Cast/Order/Ring.lean b/Mathlib/Data/Nat/Cast/Order/Ring.lean
@@ -0,0 +1,105 @@
+/-
+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.Order.Basic
+import Mathlib.Data.Nat.Cast.Basic
+import Mathlib.Algebra.CharZero.Defs
+import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Data.Nat.Cast.NeZero
+import Mathlib.Algebra.Order.Ring.Nat
+
+#align_import data.nat.cast.basic from "leanprover-community/mathlib"@"acebd8d49928f6ed8920e502a6c90674e75bd441"
+
+/-!
+# Cast of natural numbers: lemmas about bundled ordered semirings
+
+-/
+
+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 [AddMonoidWithOne α] [PartialOrder α]
+variable [CovariantClass α α (· + ·) (· ≤ ·)] [ZeroLEOneClass α]
+
+/-- 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
+
+/-- 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 : α)]
+
+/-- 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
+
+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
+
diff --git a/Mathlib/Data/Nat/Cast/SetInterval.lean b/Mathlib/Data/Nat/Cast/SetInterval.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Order.Ring.Int
-import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Order.UpperLower.Basic
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Data.Nat.Cast.Order.Basic
 
 /-!
 # Images of intervals under `Nat.cast : ℕ → ℤ`

diff --git a/Mathlib/Data/Nat/Choose/Bounds.lean b/Mathlib/Data/Nat/Choose/Bounds.lean
@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Eric Rodriguez
 -/
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Basic
 import Mathlib.Data.Nat.Choose.Basic
-import Mathlib.Data.Nat.Cast.Order
 
 #align_import data.nat.choose.bounds from "leanprover-community/mathlib"@"550b58538991c8977703fdeb7c9d51a5aa27df11"
 

diff --git a/Mathlib/ModelTheory/Algebra/Field/Basic.lean b/Mathlib/ModelTheory/Algebra/Field/Basic.lean
@@ -8,6 +8,7 @@ import Mathlib.ModelTheory.Syntax
 import Mathlib.ModelTheory.Semantics
 import Mathlib.ModelTheory.Algebra.Ring.Basic
 import Mathlib.Algebra.Field.MinimalAxioms
+import Mathlib.Data.Nat.Cast.Order.Ring
 
 /-!
 

diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -5,11 +5,12 @@ Authors: Johannes Hölzl, Mario Carneiro, Floris van Doorn
 -/
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Finsupp.Defs
-import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Data.Set.Countable
 import Mathlib.Logic.Small.Set
 import Mathlib.Order.SuccPred.CompleteLinearOrder
 import Mathlib.SetTheory.Cardinal.SchroederBernstein
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Data.Nat.Cast.Order.Basic
 
 #align_import set_theory.cardinal.basic from "leanprover-community/mathlib"@"3ff3f2d6a3118b8711063de7111a0d77a53219a8"
 

diff --git a/Mathlib/Tactic/Linarith/Lemmas.lean b/Mathlib/Tactic/Linarith/Lemmas.lean
@@ -7,7 +7,7 @@ import Batteries.Tactic.Lint.Basic
 import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.ZeroLEOne
-import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Nat.Cast.Order.Ring
 import Mathlib.Init.Data.Int.Order
 
 /-!