feat(Data/Int): port data.int.basic from the lean3 prelude (#23)

* port lean3 core's int/basic.lean

* refactor(Int): undo my strange naming

* add coe_nat_inj which I apparantly forgot about

* minor cleanup

* add missing imports

* cleanup proofs, implementing kevin's suggestions

Co-authored-by: Deniz Aydin <40861512+BeesNation@users.noreply.github.com>

Author: denayd

Mathlib.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.ByteArray
 import Mathlib.Data.Char
 import Mathlib.Data.Equiv.Basic
 import Mathlib.Data.Equiv.Functor
+import Mathlib.Data.Int.Basic
 import Mathlib.Data.List.Basic
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Gcd

Mathlib/Algebra/Group/Defs.lean

@@ -1,4 +1,5 @@
 import Mathlib.Data.Nat.Basic -- *only* for notation ℕ which should be in a "prelude"
+import Mathlib.Data.Int.Basic -- *only* for notation ℤ which should be in a "prelude"
 import Mathlib.Tactic.Spread
 
 /-!
@@ -60,9 +61,6 @@ end nat_action
 
 section int_action
 
--- TODO -- this should be in a prelude
-notation "ℤ" => Int
-
 /-- The fundamental scalar multiplication in an additive group. `gsmul_rec n a = a+a+...+a` n
 times, for integer `n`. Use instead `n • a`, which has better definitional behavior. -/
 def gsmul_rec {G : Type u} [Zero G] [Add G] [Neg G]: ℤ → G → G