chore: separate NeZero dependency from Nat/Cast/Defs (#6955)

I'm trying to remove any extraneous material from the core definitions in the algebraic hierarchy that are used in tactics.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -1601,6 +1601,7 @@ import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Data.Nat.Cast.Defs
 import Mathlib.Data.Nat.Cast.Field
+import Mathlib.Data.Nat.Cast.NeZero
 import Mathlib.Data.Nat.Cast.Prod
 import Mathlib.Data.Nat.Cast.WithTop
 import Mathlib.Data.Nat.Choose.Basic

Mathlib/Algebra/CharZero/Defs.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Tactic.NormCast.Tactic
+import Mathlib.Algebra.NeZero
 
 #align_import algebra.char_zero.defs from "leanprover-community/mathlib"@"d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d"
 

Mathlib/Algebra/Ring/Defs.lean

@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Ne
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Logic.Nontrivial
 
 #align_import algebra.ring.defs from "leanprover-community/mathlib"@"76de8ae01554c3b37d66544866659ff174e66e1f"
 

Mathlib/Data/Nat/Cast/Basic.lean

@@ -9,6 +9,7 @@ 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"

Mathlib/Data/Nat/Cast/Defs.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Algebra.NeZero
 
 #align_import data.nat.cast.defs from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
@@ -207,22 +206,6 @@ protected def AddMonoidWithOne.binary {R : Type*} [AddMonoid R] [One R] : AddMon
       rw [Nat.binCast_eq, Nat.binCast_eq, Nat.cast_succ] }
 #align add_monoid_with_one.binary AddMonoidWithOne.binary
 
-namespace NeZero
-
-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
-
-lemma of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [h : NeZero (n : R)] : NeZero n :=
-  ⟨by rintro rfl; exact h.out Nat.cast_zero⟩
-#align ne_zero.of_ne_zero_coe NeZero.of_neZero_natCast
-
-lemma pos_of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [NeZero (n : R)] : 0 < n :=
-  Nat.pos_of_ne_zero (of_neZero_natCast R).out
-#align ne_zero.pos_of_ne_zero_coe NeZero.pos_of_neZero_natCast
-
-end NeZero
-
 theorem one_add_one_eq_two [AddMonoidWithOne α] : 1 + 1 = (2 : α) := by
   rw [←Nat.cast_one, ←Nat.cast_add]
   apply congrArg

Mathlib/Data/Nat/Cast/NeZero.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2014 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Gabriel Ebner
+-/
+import Mathlib.Data.Nat.Cast.Defs
+import Mathlib.Algebra.NeZero
+
+/-!
+# Lemmas about nonzero elements of an `AddMonoidWithOne`
+-/
+
+namespace NeZero
+
+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
+
+lemma of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [h : NeZero (n : R)] : NeZero n :=
+  ⟨by rintro rfl; exact h.out Nat.cast_zero⟩
+#align ne_zero.of_ne_zero_coe NeZero.of_neZero_natCast
+
+lemma pos_of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [NeZero (n : R)] : 0 < n :=
+  Nat.pos_of_ne_zero (of_neZero_natCast R).out
+#align ne_zero.pos_of_ne_zero_coe NeZero.pos_of_neZero_natCast
+
+end NeZero