From 72a9c71e8537c67b3dc29bcd70bf29bb274a640b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 4 Apr 2023 07:35:52 +0000
Subject: [PATCH 01/13] =?UTF-8?q?feat:=20`a/c=20=E2=89=A1=20b/c=20mod=20m/?=
 =?UTF-8?q?c=20=E2=86=92=20a=20=E2=89=A1=20b=20mod=20m`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Algebra/CharP/Basic.lean       | 19 ++++---
 Mathlib/Algebra/Ring/Divisibility.lean |  5 +-
 Mathlib/Data/Int/GCD.lean              | 16 +++---
 Mathlib/Data/Int/ModEq.lean            | 78 ++++++++++++++++++++------
 Mathlib/Data/Nat/ModEq.lean            |  6 +-
 Mathlib/Data/Nat/Order/Lemmas.lean     | 11 +++-
 Mathlib/Data/ZMod/Basic.lean           | 31 +++++++++-
 7 files changed, 127 insertions(+), 39 deletions(-)

diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index 3b45978444a74..cf1980632d9fb 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Joey van Langen, Casper Putz
 
 ! This file was ported from Lean 3 source module algebra.char_p.basic
-! leanprover-community/mathlib commit ceb887ddf3344dab425292e497fa2af91498437c
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -141,10 +141,17 @@ theorem CharP.int_cast_eq_zero_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a
     rw [Int.cast_ofNat, CharP.cast_eq_zero_iff R p, Int.coe_nat_dvd]
 #align char_p.int_cast_eq_zero_iff CharP.int_cast_eq_zero_iff
 
-theorem CharP.int_cast_eq_int_cast_iff [AddGroupWithOne R] (p : ℕ) [CharP R p] (a b : ℤ) :
-    (a : R) = (b : R) ↔ a ≡ b [ZMOD p] := by
+theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℤ} :
+    (a : R) = b ↔ a ≡ b [ZMOD p] := by
   rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
-#align char_p.int_coe_eq_int_coe_iff CharP.int_cast_eq_int_cast_iff
+#align char_p.int_cast_eq_int_cast CharP.intCast_eq_intCast
+
+theorem CharP.natCast_eq_natCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} :
+    (a : R) = b ↔ a ≡ b [MOD p] :=
+  by
+  rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
+  exact (CharP.int_cast_eq_int_cast _ _).trans Int.coe_nat_modEq_iff
+#align char_p.nat_cast_eq_nat_cast CharP.natCast_eq_natCast
 
 theorem CharP.eq [AddMonoidWithOne R] {p q : ℕ} (_c1 : CharP R p) (_c2 : CharP R q) : p = q :=
   Nat.dvd_antisymm ((CharP.cast_eq_zero_iff R p q).1 (CharP.cast_eq_zero _ _))
@@ -286,10 +293,6 @@ theorem sub_pow_char_pow [CommRing R] {p : ℕ} [Fact p.Prime] [CharP R p] {n :
   sub_pow_char_pow_of_commute _ _ _ (Commute.all _ _)
 #align sub_pow_char_pow sub_pow_char_pow
 
-theorem eq_iff_modEq_int [Ring R] (p : ℕ) [CharP R p] (a b : ℤ) : (a : R) = b ↔ a ≡ b [ZMOD p] := by
-  rw [eq_comm, ← sub_eq_zero, ← Int.cast_sub, CharP.int_cast_eq_zero_iff R p, Int.modEq_iff_dvd]
-#align eq_iff_modeq_int eq_iff_modEq_int
-
 theorem CharP.neg_one_ne_one [Ring R] (p : ℕ) [CharP R p] [Fact (2 < p)] : (-1 : R) ≠ (1 : R) := by
   suffices (2 : R) ≠ 0 by
     intro h
diff --git a/Mathlib/Algebra/Ring/Divisibility.lean b/Mathlib/Algebra/Ring/Divisibility.lean
index 08a4bd5bf1505..35981ed9529ca 100644
--- a/Mathlib/Algebra/Ring/Divisibility.lean
+++ b/Mathlib/Algebra/Ring/Divisibility.lean
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Ne
 Ported by: Matej Penciak
 
 ! This file was ported from Lean 3 source module algebra.ring.divisibility
-! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -125,6 +125,9 @@ theorem dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ b - c) : a ∣ b ↔ a 
     exact eq_add_of_sub_eq rfl
 #align dvd_iff_dvd_of_dvd_sub dvd_iff_dvd_of_dvd_sub
 
+theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg, neg_sub]
+#align dvd_sub_comm dvd_sub_comm
+
 end NonUnitalRing
 
 section Ring
diff --git a/Mathlib/Data/Int/GCD.lean b/Mathlib/Data/Int/GCD.lean
index cd27eae7d5703..8de009892c5ee 100644
--- a/Mathlib/Data/Int/GCD.lean
+++ b/Mathlib/Data/Int/GCD.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sangwoo Jo (aka Jason), Guy Leroy, Johannes Hölzl, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.int.gcd
-! leanprover-community/mathlib commit d4f69d96f3532729da8ebb763f4bc26fcf640f06
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -306,13 +306,13 @@ theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j :
   apply Nat.gcd_mul_right
 #align int.gcd_mul_right Int.gcd_mul_right
 
-theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_left (natAbs j) (natAbs_pos.2 i_non_zero)
-#align int.gcd_pos_of_non_zero_left Int.gcd_pos_of_non_zero_left
+theorem gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < gcd i j :=
+  Nat.gcd_pos_of_pos_left _ <| natAbs_pos_of_ne_zero hi
+#align int.gcd_pos_of_ne_zero_left Int.gcd_pos_of_ne_zero_left
 
-theorem gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_right (natAbs i) (natAbs_pos.2 j_non_zero)
-#align int.gcd_pos_of_non_zero_right Int.gcd_pos_of_non_zero_right
+theorem gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < gcd i j :=
+  Nat.gcd_pos_of_pos_right _ <| natAbs_pos_of_ne_zero hj
+#align int.gcd_pos_of_ne_zero_right Int.gcd_pos_of_ne_zero_right
 
 theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by
   rw [gcd, Nat.gcd_eq_zero_iff, natAbs_eq_zero, natAbs_eq_zero]
@@ -430,7 +430,7 @@ theorem gcd_least_linear {a b : ℤ} (ha : a ≠ 0) :
     IsLeast { n : ℕ | 0 < n ∧ ∃ x y : ℤ, ↑n = a * x + b * y } (a.gcd b) := by
   simp_rw [← gcd_dvd_iff]
   constructor
-  · simpa [and_true_iff, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_non_zero_left b ha
+  · simpa [and_true_iff, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha
   · simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
     exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn
 #align int.gcd_least_linear Int.gcd_least_linear
diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index b755f7c6e6820..8f145e85334f3 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module data.int.modeq
-! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -69,8 +69,14 @@ protected theorem trans : a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMO
 instance : IsTrans ℤ (ModEq n) where
   trans := @Int.ModEq.trans n
 
+protected theorem eq : a ≡ b [ZMOD n] → a % n = b % n := id
+#align int.modeq.eq Int.ModEq.eq
+
 end ModEq
 
+theorem modEq_comm : a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n] := ⟨ModEq.symm, ModEq.symm⟩
+#align int.modeq_comm Int.modEq_comm
+
 theorem coe_nat_modEq_iff {a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] := by
   unfold ModEq Nat.ModEq; rw [← Int.ofNat_inj]; simp [coe_nat_mod]
 #align int.coe_nat_modeq_iff Int.coe_nat_modEq_iff
@@ -106,23 +112,31 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
   emod_emod _ _
 #align int.mod_modeq Int.mod_modEq
 
+@[simp]
+theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by simp [modeq_iff_dvd, dvd_sub_comm]
+#align int.neg_modeq_neg Int.neg_modEq_neg
+
+@[simp]
+theorem modEq_neg : a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] := by simp [modeq_iff_dvd]
+#align int.modeq_neg Int.modEq_neg
+
 namespace ModEq
 
 protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m] :=
   modEq_iff_dvd.2 <| d.trans h.dvd
 #align int.modeq.of_dvd Int.ModEq.of_dvd
 
-protected theorem mul_left' (hc : 0 ≤ c) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
-  match hc.lt_or_eq with
-  | .inl hc => by
-    unfold ModEq
-    simp [mul_emod_mul_of_pos _ _ hc, show _ = _ from h]
-  | .inr hc => by
-    simp [hc.symm]
+protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
+  by
+  obtain hc | rfl | hc := lt_trichotomy c 0
+  · rw [← neg_modeq_neg, ← modeq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
+    simp only [modeq, mul_mod_mul_of_pos (neg_pos.2 hc), h.eq]
+  · simp
+  · simp only [modeq, mul_mod_mul_of_pos hc, h.eq]
 #align int.modeq.mul_left' Int.ModEq.mul_left'
 
-protected theorem mul_right' (hc : 0 ≤ c) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
-  rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left' hc
+protected theorem mul_right' (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
+  rw [mul_comm a, mul_comm b, mul_comm n] <;> exact h.mul_left'
 #align int.modeq.mul_right' Int.ModEq.mul_right'
 
 protected theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
@@ -179,16 +193,11 @@ protected theorem sub_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a - c ≡ b - c [
 #align int.modeq.sub_right Int.ModEq.sub_right
 
 protected theorem mul_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD n] :=
-  match (le_total 0 c) with
-  | .inl hc => (h.mul_left' hc).of_dvd (dvd_mul_left _ _)
-  | .inr hc => by
-    rw [← neg_neg c, neg_mul, neg_mul _ b]
-    exact ((h.mul_left' <| neg_nonneg.2 hc).of_dvd (dvd_mul_left _ _)).neg
+  h.mul_left'.of_dvd <| dvd_mul_left _ _
 #align int.modeq.mul_left Int.ModEq.mul_left
 
 protected theorem mul_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] := by
-  rw [mul_comm a, mul_comm b]
-  exact h.mul_left c
+  h.mul_right'.of_dvd <| dvd_mul_right _ _
 #align int.modeq.mul_right Int.ModEq.mul_right
 
 protected theorem mul (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] :=
@@ -209,6 +218,29 @@ lemma of_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
   mul_comm m n ▸ of_mul_left _
 #align int.modeq.of_mul_right Int.ModEq.of_mul_right
 
+/-- To cancel a common factor `c` from a `modeq` we must divide the modulus `m` by `gcd m c`. -/
+theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
+  by
+  let d := gcd m c
+  have hmd := gcd_dvd_left m c
+  have hcd := gcd_dvd_right m c
+  rw [modeq_iff_dvd] at h⊢
+  refine' Int.dvd_of_dvd_mul_right_of_gcd_one _ _
+  show m / d ∣ c / d * (b - a)
+  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
+    exact Int.ediv_dvd_ediv hmd h
+  · rw [gcd_div hmd hcd, nat_abs_of_nat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
+#align int.modeq.cancel_right_div_gcd Int.ModEq.cancel_right_div_gcd
+
+/-- To cancel a common factor `c` from a `modeq` we must divide the modulus `m` by `gcd m c`. -/
+theorem cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
+  cancel_right_div_gcd hm <| by simpa [mul_comm] using h
+#align int.modeq.cancel_left_div_gcd Int.ModEq.cancel_left_div_gcd
+
+theorem of_div (h : a / c ≡ b / c [ZMOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
+    a ≡ b [ZMOD m] := by convert h.mul_left' <;> rwa [Int.mul_ediv_cancel']
+#align int.modeq.of_div Int.ModEq.of_div
+
 end ModEq
 
 theorem modEq_one : a ≡ b [ZMOD 1] :=
@@ -219,6 +251,18 @@ theorem modEq_sub (a b : ℤ) : a ≡ b [ZMOD a - b] :=
   (modEq_of_dvd dvd_rfl).symm
 #align int.modeq_sub Int.modEq_sub
 
+@[simp]
+theorem modEq_zero_iff : a ≡ b [ZMOD 0] ↔ a = b := by rw [modeq, mod_zero, mod_zero]
+#align int.modeq_zero_iff Int.modEq_zero_iff
+
+@[simp]
+theorem add_modEq_left : n + a ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp
+#align int.add_modeq_left Int.add_modEq_left
+
+@[simp]
+theorem add_modEq_right : a + n ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp
+#align int.add_modeq_right Int.add_modEq_right
+
 theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℤ} (hmn : m.natAbs.coprime n.natAbs) :
     a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n] :=
   ⟨fun h => by
diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean
index cc0241059a764..694c76a385dad 100644
--- a/Mathlib/Data/Nat/ModEq.lean
+++ b/Mathlib/Data/Nat/ModEq.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.modeq
-! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -212,6 +212,10 @@ For cancelling right multiplication on both sides of the `≡`, see `nat.modeq.m
 lemma of_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] := mul_comm m n ▸ of_mul_left _
 #align nat.modeq.of_mul_right Nat.ModEq.of_mul_right
 
+theorem of_div (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
+    a ≡ b [MOD m] := by convert h.mul_left' c <;> rwa [Nat.mul_div_cancel']
+#align nat.modeq.of_div Nat.ModEq.of_div
+
 end ModEq
 
 lemma modEq_sub (h : b ≤ a) : a ≡ b [MOD a - b] := (modEq_of_dvd $ by rw [Int.ofNat_sub h]).symm
diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
index 55a6960f61192..9ad44498b6704 100644
--- a/Mathlib/Data/Nat/Order/Lemmas.lean
+++ b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.order.lemmas
-! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,7 +25,7 @@ please feel free to reorganize these two files.
 
 universe u v
 
-variable {m n k : ℕ}
+variable {a b m n k : ℕ}
 
 namespace Nat
 
@@ -205,6 +205,13 @@ theorem eq_zero_of_dvd_of_lt {a b : ℕ} (w : a ∣ b) (h : b < a) : b = 0 :=
     ((Nat.div_eq_zero_iff (lt_of_le_of_lt (zero_le b) h)).mpr h)
 #align nat.eq_zero_of_dvd_of_lt Nat.eq_zero_of_dvd_of_lt
 
+theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b :=
+  by
+  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
+  rw [← mul_add_one] at h
+  exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
+#align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd
+
 @[simp]
 theorem mod_div_self (m n : ℕ) : m % n / n = 0 := by
   cases n
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index dc93273aa5bdf..d8b035d387644 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module data.zmod.basic
-! leanprover-community/mathlib commit 297619ec79dedf23525458b6bf5bf35c736fd2b8
+! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -34,6 +34,7 @@ This is a ring hom if the ring has characteristic dividing `n`
 
 -/
 
+open Function
 
 namespace ZMod
 
@@ -455,7 +456,7 @@ end CharEq
 end UniversalProperty
 
 theorem int_cast_eq_int_cast_iff (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [ZMOD c] :=
-  CharP.int_cast_eq_int_cast_iff (ZMod c) c a b
+  CharP.intCast_eq_intCast (ZMod c) c a b
 #align zmod.int_coe_eq_int_coe_iff ZMod.int_cast_eq_int_cast_iff
 
 theorem int_cast_eq_int_cast_iff' (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c :=
@@ -1051,6 +1052,8 @@ theorem prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq :
     hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]
 #align zmod.prime_ne_zero ZMod.prime_ne_zero
 
++variable {n a : ℕ}
+
 theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
     a.valMinAbs.natAbs = min a.val (n - a.val) := by
   rw [valMinAbs_def_pos]
@@ -1070,6 +1073,30 @@ theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
     apply Nat.lt_succ_self
 #align zmod.val_min_abs_nat_abs_eq_min ZMod.valMinAbs_natAbs_eq_min
 
+theorem valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a := by
+  cases n
+  · simp
+  ·
+    simp [val_min_abs_def_pos, val_nat_cast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
+      ha]
+#align zmod.val_min_abs_nat_cast_of_le_half ZMod.valMinAbs_natCast_of_le_half
+
+theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
+    (a : ZMod n).valMinAbs = a - n := by
+  cases n
+  · cases not_lt_bot ha'
+  · simp [val_min_abs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]
+#align zmod.val_min_abs_nat_cast_of_half_lt ZMod.valMinAbs_natCast_of_half_lt
+
+--porting note: There was an extraneous `nat_` in the mathlib name
+@[simp]
+theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 :=
+  by
+  refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩
+  rw [← Int.natAbs_ofNat a, ← ha]
+  exact natAbs_valMinAbs_le a
+#align zmod.val_min_nat_abs_nat_cast_eq_self ZMod.valMinAbs_natCast_eq_self
+
 theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
     x.natAbs ≤ y.natAbs := by
   rw [int_cast_eq_int_cast_iff_dvd_sub] at he

From abb70ec8493212713adf4272460040c257f3c36c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 5 Apr 2023 07:02:32 +0000
Subject: [PATCH 02/13] fix algebra.ring.divisibility

---
 Mathlib/Algebra/Ring/Divisibility.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Ring/Divisibility.lean b/Mathlib/Algebra/Ring/Divisibility.lean
index 35981ed9529ca..d90aad4077e5c 100644
--- a/Mathlib/Algebra/Ring/Divisibility.lean
+++ b/Mathlib/Algebra/Ring/Divisibility.lean
@@ -125,7 +125,8 @@ theorem dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ b - c) : a ∣ b ↔ a 
     exact eq_add_of_sub_eq rfl
 #align dvd_iff_dvd_of_dvd_sub dvd_iff_dvd_of_dvd_sub
 
-theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg, neg_sub]
+--porting note: Needed to give an explicit argument to `dvd_neg`
+theorem dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [← dvd_neg a, neg_sub]
 #align dvd_sub_comm dvd_sub_comm
 
 end NonUnitalRing

From e6ab2c4e3576d675825196adf32cd8a15d30d517 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 5 Apr 2023 07:27:51 +0000
Subject: [PATCH 03/13] fix data.nat.order.lemmas

---
 Mathlib/Data/Nat/Order/Lemmas.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
index 9ad44498b6704..45cd09c673298 100644
--- a/Mathlib/Data/Nat/Order/Lemmas.lean
+++ b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -205,10 +205,11 @@ theorem eq_zero_of_dvd_of_lt {a b : ℕ} (w : a ∣ b) (h : b < a) : b = 0 :=
     ((Nat.div_eq_zero_iff (lt_of_le_of_lt (zero_le b) h)).mpr h)
 #align nat.eq_zero_of_dvd_of_lt Nat.eq_zero_of_dvd_of_lt
 
+--porting note: Needed to give an explicit argument to `mul_add_one`
 theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b :=
   by
   rintro ⟨a, rfl⟩ ⟨b, rfl⟩
-  rw [← mul_add_one] at h
+  rw [← mul_add_one n] at h
   exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
 #align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd
 

From 40ab78eb8a1997fce08cb364c03378ae7b5e1eb8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 5 Apr 2023 12:50:54 +0000
Subject: [PATCH 04/13] fix data.int.gcd

---
 Mathlib/Data/Int/GCD.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Int/GCD.lean b/Mathlib/Data/Int/GCD.lean
index 8de009892c5ee..9c9fb3cd076a1 100644
--- a/Mathlib/Data/Int/GCD.lean
+++ b/Mathlib/Data/Int/GCD.lean
@@ -307,11 +307,11 @@ theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j :
 #align int.gcd_mul_right Int.gcd_mul_right
 
 theorem gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_left _ <| natAbs_pos_of_ne_zero hi
+  Nat.gcd_pos_of_pos_left _ $ natAbs_pos.2 hi
 #align int.gcd_pos_of_ne_zero_left Int.gcd_pos_of_ne_zero_left
 
 theorem gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < gcd i j :=
-  Nat.gcd_pos_of_pos_right _ <| natAbs_pos_of_ne_zero hj
+  Nat.gcd_pos_of_pos_right _ $ natAbs_pos.2 hj
 #align int.gcd_pos_of_ne_zero_right Int.gcd_pos_of_ne_zero_right
 
 theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 := by

From db82ccd0dd0ec92ad93e3070b3abe49f3fa574ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 5 Apr 2023 16:10:55 +0000
Subject: [PATCH 05/13] simp neg_sub_neg

---
 Mathlib/Algebra/Group/Basic.lean |  2 +-
 Mathlib/Data/Int/ModEq.lean      | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index 24f22ac3ca274..86582722abb6c 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -496,7 +496,7 @@ theorem inv_mul' : (a * b)⁻¹ = a⁻¹ / b := by simp
 #align inv_mul' inv_mul'
 #align neg_add' neg_add'
 
-@[to_additive]
+@[to_additive (attr := simp)]
 theorem inv_div_inv : a⁻¹ / b⁻¹ = b / a := by simp
 #align inv_div_inv inv_div_inv
 #align neg_sub_neg neg_sub_neg
diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index 8f145e85334f3..e34c48df2cf36 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -113,11 +113,11 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
 #align int.mod_modeq Int.mod_modEq
 
 @[simp]
-theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by simp [modeq_iff_dvd, dvd_sub_comm]
+theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by simp [modEq_iff_dvd, dvd_sub_comm]
 #align int.neg_modeq_neg Int.neg_modEq_neg
 
 @[simp]
-theorem modEq_neg : a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] := by simp [modeq_iff_dvd]
+theorem modEq_neg : a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] := by simp [modEq_iff_dvd]
 #align int.modeq_neg Int.modEq_neg
 
 namespace ModEq
@@ -129,10 +129,10 @@ protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m]
 protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
   by
   obtain hc | rfl | hc := lt_trichotomy c 0
-  · rw [← neg_modeq_neg, ← modeq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
-    simp only [modeq, mul_mod_mul_of_pos (neg_pos.2 hc), h.eq]
+  · rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
+    simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
   · simp
-  · simp only [modeq, mul_mod_mul_of_pos hc, h.eq]
+  · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]
 #align int.modeq.mul_left' Int.ModEq.mul_left'
 
 protected theorem mul_right' (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
@@ -224,7 +224,7 @@ theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡
   let d := gcd m c
   have hmd := gcd_dvd_left m c
   have hcd := gcd_dvd_right m c
-  rw [modeq_iff_dvd] at h⊢
+  rw [modEq_iff_dvd] at h⊢
   refine' Int.dvd_of_dvd_mul_right_of_gcd_one _ _
   show m / d ∣ c / d * (b - a)
   · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]

From 8e751c5ba7bbf53f88880104d2a86543e8f06fc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 6 Apr 2023 09:13:46 +0000
Subject: [PATCH 06/13] fixes

---
 Mathlib/Algebra/CharP/Basic.lean |  5 ++---
 Mathlib/Data/Int/ModEq.lean      | 19 +++++++++++--------
 Mathlib/Data/ZMod/Basic.lean     | 12 +++++-------
 3 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index cf1980632d9fb..62732d1f94a16 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -147,10 +147,9 @@ theorem CharP.intCast_eq_intCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b
 #align char_p.int_cast_eq_int_cast CharP.intCast_eq_intCast
 
 theorem CharP.natCast_eq_natCast [AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} :
-    (a : R) = b ↔ a ≡ b [MOD p] :=
-  by
+    (a : R) = b ↔ a ≡ b [MOD p] := by
   rw [← Int.cast_ofNat, ← Int.cast_ofNat b]
-  exact (CharP.int_cast_eq_int_cast _ _).trans Int.coe_nat_modEq_iff
+  exact (CharP.intCast_eq_intCast _ _).trans Int.coe_nat_modEq_iff
 #align char_p.nat_cast_eq_nat_cast CharP.natCast_eq_natCast
 
 theorem CharP.eq [AddMonoidWithOne R] {p q : ℕ} (_c1 : CharP R p) (_c2 : CharP R q) : p = q :=
diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index e34c48df2cf36..8eee775352812 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -113,7 +113,8 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
 #align int.mod_modeq Int.mod_modEq
 
 @[simp]
-theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by simp [modEq_iff_dvd, dvd_sub_comm]
+theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
+  simp [-sub_neg_eq_add, modEq_iff_dvd, dvd_sub_comm]
 #align int.neg_modeq_neg Int.neg_modEq_neg
 
 @[simp]
@@ -126,8 +127,7 @@ protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m]
   modEq_iff_dvd.2 <| d.trans h.dvd
 #align int.modeq.of_dvd Int.ModEq.of_dvd
 
-protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=
-  by
+protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] := by
   obtain hc | rfl | hc := lt_trichotomy c 0
   · rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
     simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
@@ -136,7 +136,7 @@ protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n
 #align int.modeq.mul_left' Int.ModEq.mul_left'
 
 protected theorem mul_right' (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
-  rw [mul_comm a, mul_comm b, mul_comm n] <;> exact h.mul_left'
+  rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left'
 #align int.modeq.mul_right' Int.ModEq.mul_right'
 
 protected theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
@@ -196,7 +196,7 @@ protected theorem mul_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [Z
   h.mul_left'.of_dvd <| dvd_mul_left _ _
 #align int.modeq.mul_left Int.ModEq.mul_left
 
-protected theorem mul_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] := by
+protected theorem mul_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] :=
   h.mul_right'.of_dvd <| dvd_mul_right _ _
 #align int.modeq.mul_right Int.ModEq.mul_right
 
@@ -218,7 +218,7 @@ lemma of_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
   mul_comm m n ▸ of_mul_left _
 #align int.modeq.of_mul_right Int.ModEq.of_mul_right
 
-/-- To cancel a common factor `c` from a `modeq` we must divide the modulus `m` by `gcd m c`. -/
+/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
 theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
   by
   let d := gcd m c
@@ -226,13 +226,16 @@ theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡
   have hcd := gcd_dvd_right m c
   rw [modEq_iff_dvd] at h⊢
   refine' Int.dvd_of_dvd_mul_right_of_gcd_one _ _
+  -- porting note: The `show` below doesn't assign the metavariable properly, so we need an extra
+  -- `swap`
+  swap
   show m / d ∣ c / d * (b - a)
   · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
     exact Int.ediv_dvd_ediv hmd h
-  · rw [gcd_div hmd hcd, nat_abs_of_nat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
+  · rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
 #align int.modeq.cancel_right_div_gcd Int.ModEq.cancel_right_div_gcd
 
-/-- To cancel a common factor `c` from a `modeq` we must divide the modulus `m` by `gcd m c`. -/
+/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
 theorem cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
   cancel_right_div_gcd hm <| by simpa [mul_comm] using h
 #align int.modeq.cancel_left_div_gcd Int.ModEq.cancel_left_div_gcd
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index d8b035d387644..489813255407b 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -456,7 +456,7 @@ end CharEq
 end UniversalProperty
 
 theorem int_cast_eq_int_cast_iff (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a ≡ b [ZMOD c] :=
-  CharP.intCast_eq_intCast (ZMod c) c a b
+  CharP.intCast_eq_intCast (ZMod c) c
 #align zmod.int_coe_eq_int_coe_iff ZMod.int_cast_eq_int_cast_iff
 
 theorem int_cast_eq_int_cast_iff' (a b : ℤ) (c : ℕ) : (a : ZMod c) = (b : ZMod c) ↔ a % c = b % c :=
@@ -1052,7 +1052,7 @@ theorem prime_ne_zero (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq :
     hp.1.coprime_iff_not_dvd, Nat.coprime_primes hp.1 hq.1]
 #align zmod.prime_ne_zero ZMod.prime_ne_zero
 
-+variable {n a : ℕ}
+variable {n a : ℕ}
 
 theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
     a.valMinAbs.natAbs = min a.val (n - a.val) := by
@@ -1076,8 +1076,7 @@ theorem valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
 theorem valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a := by
   cases n
   · simp
-  ·
-    simp [val_min_abs_def_pos, val_nat_cast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
+  · simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
       ha]
 #align zmod.val_min_abs_nat_cast_of_le_half ZMod.valMinAbs_natCast_of_le_half
 
@@ -1085,13 +1084,12 @@ theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
     (a : ZMod n).valMinAbs = a - n := by
   cases n
   · cases not_lt_bot ha'
-  · simp [val_min_abs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]
+  · simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]
 #align zmod.val_min_abs_nat_cast_of_half_lt ZMod.valMinAbs_natCast_of_half_lt
 
 --porting note: There was an extraneous `nat_` in the mathlib name
 @[simp]
-theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 :=
-  by
+theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 := by
   refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩
   rw [← Int.natAbs_ofNat a, ← ha]
   exact natAbs_valMinAbs_le a

From df36ecdab6e6e66b404ed6610f02dcc4f30f658b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 6 Apr 2023 10:39:44 +0000
Subject: [PATCH 07/13] fix data.int.modeq

---
 Mathlib/Data/Int/ModEq.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index 8eee775352812..e974a2933ed71 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -221,7 +221,7 @@ lemma of_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
 /-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
 theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
   by
-  let d := gcd m c
+  letI d := gcd m c
   have hmd := gcd_dvd_left m c
   have hcd := gcd_dvd_right m c
   rw [modEq_iff_dvd] at h⊢
@@ -255,7 +255,7 @@ theorem modEq_sub (a b : ℤ) : a ≡ b [ZMOD a - b] :=
 #align int.modeq_sub Int.modEq_sub
 
 @[simp]
-theorem modEq_zero_iff : a ≡ b [ZMOD 0] ↔ a = b := by rw [modeq, mod_zero, mod_zero]
+theorem modEq_zero_iff : a ≡ b [ZMOD 0] ↔ a = b := by rw [ModEq, emod_zero, emod_zero]
 #align int.modeq_zero_iff Int.modEq_zero_iff
 
 @[simp]

From 85e82cddc818bfa46b777c620dff9a596acce07a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Apr 2023 11:56:29 +0100
Subject: [PATCH 08/13] Update Mathlib/Data/Nat/Order/Lemmas.lean

---
 Mathlib/Data/Nat/Order/Lemmas.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
index 45cd09c673298..e12e1f9dec26e 100644
--- a/Mathlib/Data/Nat/Order/Lemmas.lean
+++ b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -205,10 +205,9 @@ theorem eq_zero_of_dvd_of_lt {a b : ℕ} (w : a ∣ b) (h : b < a) : b = 0 :=
     ((Nat.div_eq_zero_iff (lt_of_le_of_lt (zero_le b) h)).mpr h)
 #align nat.eq_zero_of_dvd_of_lt Nat.eq_zero_of_dvd_of_lt
 
---porting note: Needed to give an explicit argument to `mul_add_one`
-theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b :=
-  by
+theorem le_of_lt_add_of_dvd (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b := by
   rintro ⟨a, rfl⟩ ⟨b, rfl⟩
+  -- porting note: Needed to give an explicit argument to `mul_add_one`
   rw [← mul_add_one n] at h
   exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
 #align nat.le_of_lt_add_of_dvd Nat.le_of_lt_add_of_dvd

From 06560e7f61d693c7cf55c240dd7950ccf7f1c931 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Apr 2023 11:56:50 +0100
Subject: [PATCH 09/13] Update Mathlib/Data/ZMod/Basic.lean

---
 Mathlib/Data/ZMod/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 489813255407b..b4c037068d845 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -1087,7 +1087,7 @@ theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) :
   · simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]
 #align zmod.val_min_abs_nat_cast_of_half_lt ZMod.valMinAbs_natCast_of_half_lt
 
---porting note: There was an extraneous `nat_` in the mathlib name
+-- porting note: There was an extraneous `nat_` in the mathlib3 name
 @[simp]
 theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 := by
   refine' ⟨fun ha => _, valMinAbs_natCast_of_le_half⟩

From e52336c542696dd3c1c133b9ec5f4aa2439e65bd Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 6 Apr 2023 11:10:18 +0000
Subject: [PATCH 10/13] remove confusing porting note

---
 Mathlib/Data/Int/ModEq.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index e974a2933ed71..6f1fd13a2889b 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -224,12 +224,9 @@ theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡
   letI d := gcd m c
   have hmd := gcd_dvd_left m c
   have hcd := gcd_dvd_right m c
-  rw [modEq_iff_dvd] at h⊢
-  refine' Int.dvd_of_dvd_mul_right_of_gcd_one _ _
-  -- porting note: The `show` below doesn't assign the metavariable properly, so we need an extra
-  -- `swap`
-  swap
-  show m / d ∣ c / d * (b - a)
+  rw [modEq_iff_dvd] at h ⊢
+  -- porting note: removed `show` due to leanprover-community/mathlib4#3305
+  refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
   · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
     exact Int.ediv_dvd_ediv hmd h
   · rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]

From 8aefd69657c0052d0709ee6dc482f55bb196c3ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 6 Apr 2023 16:01:24 +0000
Subject: [PATCH 11/13] fix data.int.modeq

---
 Mathlib/Data/Int/ModEq.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index 6f1fd13a2889b..6d140f1d8ecdc 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -114,7 +114,8 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
 
 @[simp]
 theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
-  simp [-sub_neg_eq_add, modEq_iff_dvd, dvd_sub_comm]
+--porting note: Restore old proof once #3309 is through
+  simp [neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
 #align int.neg_modeq_neg Int.neg_modEq_neg
 
 @[simp]

From af5877e2b7b244c898b8d525a4aa784eeec11a65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 6 Apr 2023 16:02:23 +0000
Subject: [PATCH 12/13] revert algebra.group.basic

---
 Mathlib/Algebra/Group/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index 86582722abb6c..24f22ac3ca274 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -496,7 +496,7 @@ theorem inv_mul' : (a * b)⁻¹ = a⁻¹ / b := by simp
 #align inv_mul' inv_mul'
 #align neg_add' neg_add'
 
-@[to_additive (attr := simp)]
+@[to_additive]
 theorem inv_div_inv : a⁻¹ / b⁻¹ = b / a := by simp
 #align inv_div_inv inv_div_inv
 #align neg_sub_neg neg_sub_neg

From 44d066f697ef0943523772dfbe89eebfd757ae89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 6 Apr 2023 17:51:39 +0000
Subject: [PATCH 13/13] fix data.int.modeq

---
 Mathlib/Data/Int/ModEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index 6d140f1d8ecdc..257b3ff4b92d8 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -115,7 +115,7 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
 @[simp]
 theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
 --porting note: Restore old proof once #3309 is through
-  simp [neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
+  simp [-sub_neg_eq_add, neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
 #align int.neg_modeq_neg Int.neg_modEq_neg
 
 @[simp]