feat: add some docstrings to lemmas specialized to Nat and Int (#11694)

Mathlib/Data/Int/GCD.lean

@@ -224,10 +224,14 @@ theorem natAbs_ediv (a b : ℤ) (H : b ∣ a) : natAbs (a / b) = natAbs a / natA
     _ = natAbs a / natAbs b := by rw [Int.ediv_mul_cancel H]
 #align int.nat_abs_div Int.natAbs_ediv
 
+/-- special case of `mul_dvd_mul_iff_right` for `ℤ`.
+Duplicated here to keep simple imports for this file. -/
 theorem dvd_of_mul_dvd_mul_left {i j k : ℤ} (k_non_zero : k ≠ 0) (H : k * i ∣ k * j) : i ∣ j :=
   Dvd.elim H fun l H1 => by rw [mul_assoc] at H1; exact ⟨_, mul_left_cancel₀ k_non_zero H1⟩
 #align int.dvd_of_mul_dvd_mul_left Int.dvd_of_mul_dvd_mul_left
 
+/-- special case of `mul_dvd_mul_iff_right` for `ℤ`.
+Duplicated here to keep simple imports for this file. -/
 theorem dvd_of_mul_dvd_mul_right {i j k : ℤ} (k_non_zero : k ≠ 0) (H : i * k ∣ j * k) : i ∣ j := by
   rw [mul_comm i k, mul_comm j k] at H; exact dvd_of_mul_dvd_mul_left k_non_zero H
 #align int.dvd_of_mul_dvd_mul_right Int.dvd_of_mul_dvd_mul_right

Mathlib/Data/Nat/Defs.lean

@@ -10,6 +10,7 @@ import Mathlib.Tactic.Cases
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.PushNeg
 import Mathlib.Tactic.Use
+import Mathlib.Util.AssertExists
 
 #align_import data.nat.basic from "leanprover-community/mathlib"@"bd835ef554f37ef9b804f0903089211f89cb370b"
 
@@ -42,6 +43,9 @@ The names of this file, `Data.Nat.Basic` and `Data.Nat.Order.Basic` are archaic
 with reality anymore. Rename them.
 -/
 
+/- We don't want to import the algebraic hierarchy in this file. -/
+assert_not_exists Monoid
+
 open Function
 
 namespace Nat
@@ -1123,10 +1127,14 @@ protected lemma dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b := (Nat.dvd
 protected lemma dvd_add_right (h : a ∣ b) : a ∣ b + c ↔ a ∣ c := (Nat.dvd_add_iff_right h).symm
 #align nat.dvd_add_right Nat.dvd_add_right
 
+/-- special case of `mul_dvd_mul_iff_left` for `ℕ`.
+Duplicated here to keep simple imports for this file. -/
 protected lemma mul_dvd_mul_iff_left (ha : 0 < a) : a * b ∣ a * c ↔ b ∣ c :=
   exists_congr fun d ↦ by rw [Nat.mul_assoc, Nat.mul_right_inj $ ne_of_gt ha]
 #align nat.mul_dvd_mul_iff_left Nat.mul_dvd_mul_iff_left
 
+/-- special case of `mul_dvd_mul_iff_right` for `ℕ`.
+Duplicated here to keep simple imports for this file. -/
 protected lemma mul_dvd_mul_iff_right (hc : 0 < c) : a * c ∣ b * c ↔ a ∣ b :=
   exists_congr fun d ↦ by rw [Nat.mul_right_comm, Nat.mul_left_inj $ ne_of_gt hc]
 #align nat.mul_dvd_mul_iff_right Nat.mul_dvd_mul_iff_right