chore: Split Data.{Nat,Int}{.Order}.Basic in group vs ring instances (#11924)

Scatter the content of `Data.Nat.Basic` across:
* `Data.Nat.Defs` for the lemmas having no dependencies
* `Algebra.Group.Nat` for the monoid instances and the few miscellaneous lemmas needing them.
* `Algebra.Ring.Nat` for the semiring instance and the few miscellaneous lemmas following it.

Similarly, scatter
* `Data.Int.Basic` across `Data.Int.Defs`, `Algebra.Group.Int`, `Algebra.Ring.Int`
* `Data.Nat.Order.Basic` across `Data.Nat.Defs`, `Algebra.Order.Group.Nat`, `Algebra.Order.Ring.Nat`
* `Data.Int.Order.Basic` across `Data.Int.Defs`, `Algebra.Order.Group.Int`, `Algebra.Order.Ring.Int`

Also move a few lemmas from `Data.Nat.Order.Lemmas` to `Data.Nat.Defs`.

Before
![pre_11924](https://github.com/leanprover-community/mathlib4/assets/14090593/be8a6259-9d2d-434d-b4a5-f5667feb9e1d)

After
![post_11924](https://github.com/leanprover-community/mathlib4/assets/14090593/3944f37f-8cfd-4254-830b-d0dbcd23b50a)

Author: YaelDillies

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -134,7 +134,7 @@ def List.dropUntil {α} [DecidableEq α] : List α → List α → List α
 open Lean Elab in
 /-- `guard_decl na mod` makes sure that the declaration with name `na` is in the module `mod`.
 ```lean
-guard_decl Nat.nontrivial Mathlib.Data.Nat.Basic -- does nothing
+guard_decl Nat.nontrivial Mathlib.Algebra.Ring.Nat -- does nothing
 
 guard_decl Nat.nontrivial Not.In.Here
 -- the module Not.In.Here is not imported!

Mathlib.lean

@@ -195,7 +195,9 @@ import Mathlib.Algebra.Group.Hom.CompTypeclasses
 import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.Group.Hom.Instances
 import Mathlib.Algebra.Group.InjSurj
+import Mathlib.Algebra.Group.Int
 import Mathlib.Algebra.Group.MinimalAxioms
+import Mathlib.Algebra.Group.Nat
 import Mathlib.Algebra.Group.NatPowAssoc
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.OrderSynonym
@@ -431,8 +433,10 @@ import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.DenselyOrdered
 import Mathlib.Algebra.Order.Group.InjSurj
 import Mathlib.Algebra.Order.Group.Instances
+import Mathlib.Algebra.Order.Group.Int
 import Mathlib.Algebra.Order.Group.Lattice
 import Mathlib.Algebra.Order.Group.MinMax
+import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Order.Group.OrderIso
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
@@ -479,7 +483,9 @@ import Mathlib.Algebra.Order.Ring.CharZero
 import Mathlib.Algebra.Order.Ring.Cone
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.Ring.InjSurj
+import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Algebra.Order.Ring.Lemmas
+import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Algebra.Order.Ring.Pow
 import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Algebra.Order.Ring.WithTop
@@ -559,7 +565,9 @@ import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
 import Mathlib.Algebra.Ring.Idempotents
 import Mathlib.Algebra.Ring.InjSurj
+import Mathlib.Algebra.Ring.Int
 import Mathlib.Algebra.Ring.MinimalAxioms
+import Mathlib.Algebra.Ring.Nat
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Algebra.Ring.OrderSynonym
 import Mathlib.Algebra.Ring.Pi
@@ -1806,7 +1814,6 @@ import Mathlib.Data.HashMap
 import Mathlib.Data.Holor
 import Mathlib.Data.Int.AbsoluteValue
 import Mathlib.Data.Int.Associated
-import Mathlib.Data.Int.Basic
 import Mathlib.Data.Int.Bitwise
 import Mathlib.Data.Int.CardIntervalMod
 import Mathlib.Data.Int.Cast.Basic
@@ -1827,7 +1834,6 @@ import Mathlib.Data.Int.Lemmas
 import Mathlib.Data.Int.Log
 import Mathlib.Data.Int.ModEq
 import Mathlib.Data.Int.NatPrime
-import Mathlib.Data.Int.Order.Basic
 import Mathlib.Data.Int.Order.Lemmas
 import Mathlib.Data.Int.Order.Units
 import Mathlib.Data.Int.Parity
@@ -1931,7 +1937,6 @@ import Mathlib.Data.Multiset.Sym
 import Mathlib.Data.NNRat.BigOperators
 import Mathlib.Data.NNRat.Defs
 import Mathlib.Data.NNRat.Lemmas
-import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Cast.Basic
@@ -1981,7 +1986,6 @@ import Mathlib.Data.Nat.MaxPowDiv
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Nat.Multiplicity
 import Mathlib.Data.Nat.Nth
-import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Data.Nat.PSub
 import Mathlib.Data.Nat.Pairing

Mathlib/Algebra/BigOperators/List/Basic.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
 import Mathlib.Algebra.Ring.Commute
-import Mathlib.Data.Int.Basic
+import Mathlib.Algebra.Ring.Int
+import Mathlib.Algebra.Ring.Nat
 import Mathlib.Data.List.Dedup
 import Mathlib.Data.List.ProdSigma
 import Mathlib.Data.List.Join
 import Mathlib.Data.List.Perm
 import Mathlib.Data.List.Range
 import Mathlib.Data.List.Rotate
-import Mathlib.Data.Nat.Basic
 
 #align_import data.list.big_operators.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
 

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -5,8 +5,10 @@ Authors: Louis Carlin, Mario Carneiro
 -/
 import Mathlib.Algebra.EuclideanDomain.Defs
 import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.Group.Nat
 import Mathlib.Algebra.GroupWithZero.Units.Basic
-import Mathlib.Data.Int.Order.Basic
+import Mathlib.Algebra.Order.Group.Int
+import Mathlib.Algebra.Ring.Int
 
 #align_import algebra.euclidean_domain.instances from "leanprover-community/mathlib"@"e1bccd6e40ae78370f01659715d3c948716e3b7e"
 

Mathlib/Data/Int/Basic.lean renamed to Mathlib/Algebra/Group/Int.lean

@@ -4,34 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import Mathlib.Algebra.Group.TypeTags
-import Mathlib.Algebra.Ring.Defs
-import Mathlib.Data.Int.Cast.Basic
 import Mathlib.Order.Monotone.Basic
 
 #align_import data.int.basic from "leanprover-community/mathlib"@"00d163e35035c3577c1c79fa53b68de17781ffc1"
 
 /-!
-# Basic algebraic instances on the integers
+# The integers form a group
 
-This file contains instances on `ℤ`. The stronger one is `Int.linearOrderedCommRing`.
+This file contains the additive group and multiplicative monoid instances on the integers.
+
+See note [foundational algebra order theory].
 -/
 
+assert_not_exists Ring
+
 open Nat
 
 namespace Int
 
-instance instCommRingInt : CommRing ℤ where
-  zero_mul := Int.zero_mul
-  mul_zero := Int.mul_zero
+/-! ### Instances -/
+
+instance instCommMonoidInt : CommMonoid ℤ where
   mul_comm := Int.mul_comm
-  left_distrib := Int.mul_add
-  right_distrib := Int.add_mul
   mul_one := Int.mul_one
   one_mul := Int.one_mul
   npow n x := x ^ n
   npow_zero _ := rfl
-  npow_succ n x := rfl
+  npow_succ _ _ := rfl
   mul_assoc := Int.mul_assoc
+
+instance instAddCommGroup : AddCommGroup ℤ where
   add_comm := Int.add_comm
   add_assoc := Int.add_assoc
   add_zero := Int.add_zero
@@ -48,54 +50,27 @@ instance instCommRingInt : CommRing ℤ where
     simp only [ofNat_eq_coe, ofNat_succ, Int.add_mul, Int.add_comm, Int.one_mul]
   zsmul_neg' m n := by simp only [negSucc_coe, ofNat_succ, Int.neg_mul]
   sub_eq_add_neg _ _ := Int.sub_eq_add_neg
-  natCast := (·)
-  natCast_zero := rfl
-  natCast_succ _ := rfl
-  intCast := (·)
-  intCast_ofNat _ := rfl
-  intCast_negSucc _ := rfl
-
-@[simp, norm_cast] lemma cast_id {n : ℤ} : Int.cast n = n := rfl
-
-@[simp, norm_cast]
-theorem cast_mul {α : Type*} [NonAssocRing α] : ∀ m n, ((m * n : ℤ) : α) = m * n := fun m => by
-  obtain ⟨m, rfl | rfl⟩ := Int.eq_nat_or_neg m
-  · induction m with
-    | zero => simp
-    | succ m ih => simp_all [add_mul]
-  · induction m with
-    | zero => simp
-    | succ m ih => simp_all [add_mul]
-#align int.cast_mul Int.cast_mulₓ -- dubious translation, type involves HasLiftT
-
-lemma cast_Nat_cast {n : ℕ} {R : Type*} [AddGroupWithOne R] :
-    (Int.cast (Nat.cast n) : R) = Nat.cast n :=
-  Int.cast_natCast _
 
-@[simp, norm_cast] lemma cast_pow {R : Type*} [Ring R] (n : ℤ) (m : ℕ) :
-    ↑(n ^ m) = (n ^ m : R) := by
-  induction' m with m ih <;> simp [_root_.pow_succ, *]
-#align int.cast_pow Int.cast_pow
-
-/-! ### Extra instances to short-circuit type class resolution
+/-!
+### Extra instances to short-circuit type class resolution
 
 These also prevent non-computable instances like `Int.normedCommRing` being used to construct
 these instances non-computably.
 -/
+
 instance : AddCommMonoid ℤ    := by infer_instance
 instance : AddMonoid ℤ        := by infer_instance
 instance : Monoid ℤ           := by infer_instance
-instance : CommMonoid ℤ       := by infer_instance
 instance : CommSemigroup ℤ    := by infer_instance
 instance : Semigroup ℤ        := by infer_instance
-instance : AddCommGroup ℤ     := by infer_instance
 instance : AddGroup ℤ         := by infer_instance
+instance : AddCommGroup ℤ     := by infer_instance
 instance : AddCommSemigroup ℤ := by infer_instance
 instance : AddSemigroup ℤ     := by infer_instance
-instance : CommSemiring ℤ     := by infer_instance
-instance : Semiring ℤ         := by infer_instance
-instance instRingInt : Ring ℤ             := by infer_instance
-instance : Distrib ℤ          := by infer_instance
+
+/-! ### Miscellaneous lemmas -/
+
+@[simp, norm_cast] lemma cast_id {n : ℤ} : Int.cast n = n := rfl
 
 lemma natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k := by
   induction' k with k ih
@@ -131,3 +106,4 @@ lemma zsmul_int_one (n : ℤ) : n • (1 : ℤ) = n := mul_one _
 #align zsmul_int_one zsmul_int_one
 
 assert_not_exists Set.range
+assert_not_exists Ring

Mathlib/Algebra/Group/Nat.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
+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.Algebra.Group.TypeTags
+
+#align_import data.nat.basic from "leanprover-community/mathlib"@"bd835ef554f37ef9b804f0903089211f89cb370b"
+
+/-!
+# The natural numbers form a monoid
+
+This file contains the additive and multiplicative monoid instances on the natural numbers.
+
+See note [foundational algebra order theory].
+-/
+
+assert_not_exists Ring
+
+open Multiplicative
+
+namespace Nat
+
+/-! ### Instances -/
+
+instance addCommMonoid : AddCommMonoid ℕ where
+  add := Nat.add
+  add_assoc := Nat.add_assoc
+  zero := Nat.zero
+  zero_add := Nat.zero_add
+  add_zero := Nat.add_zero
+  add_comm := Nat.add_comm
+  nsmul m n := m * n
+  nsmul_zero := Nat.zero_mul
+  nsmul_succ := succ_mul
+
+instance commMonoid : CommMonoid ℕ where
+  mul := Nat.mul
+  mul_assoc := Nat.mul_assoc
+  one := Nat.succ Nat.zero
+  one_mul := Nat.one_mul
+  mul_one := Nat.mul_one
+  mul_comm := Nat.mul_comm
+  npow m n := n ^ m
+  npow_zero := Nat.pow_zero
+  npow_succ _ _ := rfl
+
+/-!
+### Extra instances to short-circuit type class resolution
+
+These also prevent non-computable instances being used to construct these instances non-computably.
+-/
+
+instance addMonoid        : AddMonoid ℕ        := by infer_instance
+instance monoid           : Monoid ℕ           := by infer_instance
+instance commSemigroup    : CommSemigroup ℕ    := by infer_instance
+instance semigroup        : Semigroup ℕ        := by infer_instance
+instance addCommSemigroup : AddCommSemigroup ℕ := by infer_instance
+instance addSemigroup     : AddSemigroup ℕ     := by infer_instance
+
+/-! ### Miscellaneous lemmas -/
+
+protected lemma nsmul_eq_mul (m n : ℕ) : m • n = m * n := rfl
+#align nat.nsmul_eq_mul Nat.nsmul_eq_mul
+
+section Multiplicative
+
+lemma toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b := mul_comm _ _
+#align nat.to_add_pow Nat.toAdd_pow
+
+@[simp] lemma ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b := (toAdd_pow _ _).symm
+#align nat.of_add_mul Nat.ofAdd_mul
+
+end Multiplicative
+end Nat

Mathlib/Algebra/Group/NatPowAssoc.lean

@@ -5,7 +5,7 @@ Authors: Scott Carnahan
 -/
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.GroupTheory.GroupAction.Prod
-import Mathlib.Data.Int.Basic
+import Mathlib.Algebra.Ring.Int
 import Mathlib.Data.Nat.Cast.Basic
 
 /-!

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
+import Mathlib.Algebra.Group.Int
+import Mathlib.Algebra.Group.Nat
 import Mathlib.Algebra.Ring.Hom.Defs
-import Mathlib.Data.Int.Basic
-import Mathlib.Data.Nat.Basic
 import Mathlib.GroupTheory.GroupAction.Opposite
 
 #align_import algebra.hom.iterate from "leanprover-community/mathlib"@"792a2a264169d64986541c6f8f7e3bbb6acb6295"

Mathlib/Algebra/GroupWithZero/Power.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.GroupWithZero.Commute
-import Mathlib.Data.Int.Order.Basic
+import Mathlib.Algebra.Order.Ring.CharZero
+import Mathlib.Algebra.Order.Ring.Int
+import Mathlib.Algebra.Order.Ring.Nat
 
 #align_import algebra.group_with_zero.power from "leanprover-community/mathlib"@"46a64b5b4268c594af770c44d9e502afc6a515cb"
 

Mathlib/Algebra/Module/Basic.lean

@@ -5,7 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
-import Mathlib.Data.Int.Basic
+import Mathlib.Algebra.Ring.Int
 import Mathlib.Data.NNRat.Defs
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Pi