diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index a038a41be7e21..2e2e38411285a 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -173,8 +173,8 @@ jobs:
         run: |
           lake exe cache get
           # We pipe the output of `lake build` to a file,
-          # and if we find " Building " in that file we kill `lake build`, and error.
-          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building " && kill $! ))
+          # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
+          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
 
       - name: build archive
         run: |
@@ -213,7 +213,7 @@ jobs:
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
 
       - name: Post comments for lean-pr-testing branch
         if: always()
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index df8da8b3aff37..0c6c034c7f0a5 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -179,8 +179,8 @@ jobs:
         run: |
           lake exe cache get
           # We pipe the output of `lake build` to a file,
-          # and if we find " Building " in that file we kill `lake build`, and error.
-          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building " && kill $! ))
+          # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
+          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
 
       - name: build archive
         run: |
@@ -219,7 +219,7 @@ jobs:
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
 
       - name: Post comments for lean-pr-testing branch
         if: always()
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 74c51d3ca8ec5..b37fc96f49e5c 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -159,8 +159,8 @@ jobs:
         run: |
           lake exe cache get
           # We pipe the output of `lake build` to a file,
-          # and if we find " Building " in that file we kill `lake build`, and error.
-          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building " && kill $! ))
+          # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
+          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
 
       - name: build archive
         run: |
@@ -199,7 +199,7 @@ jobs:
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
 
       - name: Post comments for lean-pr-testing branch
         if: always()
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
index cf82aeb995fdf..f936f9130657d 100644
--- a/.github/workflows/build_fork.yml
+++ b/.github/workflows/build_fork.yml
@@ -177,8 +177,8 @@ jobs:
         run: |
           lake exe cache get
           # We pipe the output of `lake build` to a file,
-          # and if we find " Building " in that file we kill `lake build`, and error.
-          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building " && kill $! ))
+          # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
+          lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
 
       - name: build archive
         run: |
@@ -217,7 +217,7 @@ jobs:
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
 
       - name: Post comments for lean-pr-testing branch
         if: always()
diff --git a/.gitignore b/.gitignore
index f1a7499d1f43a..b762dbaaa7498 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@
 /lake-packages
 /.cache
 .DS_Store
+/lakefile.olean
diff --git a/Archive/Imo/Imo1959Q1.lean b/Archive/Imo/Imo1959Q1.lean
index 783fe6f7e14c9..4ed41592dc450 100644
--- a/Archive/Imo/Imo1959Q1.lean
+++ b/Archive/Imo/Imo1959Q1.lean
@@ -33,6 +33,6 @@ end Imo1959Q1
 
 open Imo1959Q1
 
-theorem imo1959_q1 : ∀ n : ℕ, coprime (21 * n + 4) (14 * n + 3) := fun n =>
+theorem imo1959_q1 : ∀ n : ℕ, Coprime (21 * n + 4) (14 * n + 3) := fun n =>
   coprime_of_dvd' fun k _ h1 h2 => calculation n k h1 h2
 #align imo1959_q1 imo1959_q1
diff --git a/Archive/Wiedijk100Theorems/PerfectNumbers.lean b/Archive/Wiedijk100Theorems/PerfectNumbers.lean
index 02b1db279a033..ff1f483234934 100644
--- a/Archive/Wiedijk100Theorems/PerfectNumbers.lean
+++ b/Archive/Wiedijk100Theorems/PerfectNumbers.lean
@@ -88,7 +88,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p
   rw [Nat.perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
     isMultiplicative_sigma.map_mul_of_coprime (Nat.prime_two.coprime_pow_of_not_dvd hm).symm,
     sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf
-  rcases Nat.coprime.dvd_of_dvd_mul_left
+  rcases Nat.Coprime.dvd_of_dvd_mul_left
       (Nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (Dvd.intro _ perf) with
     ⟨j, rfl⟩
   rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf
diff --git a/GNUmakefile b/GNUmakefile
index 7998c8afc7fe2..0207857b28dca 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -13,4 +13,4 @@ test/%.run: build
 	lake env lean test/$*
 
 lint: build
-	env LEAN_ABORT_ON_PANIC=1 lake exe runLinter
+	env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
diff --git a/Mathlib/Algebra/IsPrimePow.lean b/Mathlib/Algebra/IsPrimePow.lean
index e162b8d8eefd0..8050955c70d8c 100644
--- a/Mathlib/Algebra/IsPrimePow.lean
+++ b/Mathlib/Algebra/IsPrimePow.lean
@@ -104,7 +104,7 @@ theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m
   simp only [pow_zero, ne_eq] at hm₁
 #align is_prime_pow.dvd IsPrimePow.dvd
 
-theorem Nat.disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.coprime b) :
+theorem Nat.disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) :
     Disjoint (a.divisors.filter IsPrimePow) (b.divisors.filter IsPrimePow) := by
   simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
   rintro n han _ha hn hbn _hb -
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
index aa390ff800532..90e2e1ece6371 100644
--- a/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
+++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@@ -1180,7 +1180,7 @@ lemma ofJ'_j (j : R) [Invertible j] [Invertible (j - 1728)] : (ofJ' j).j = j :=
 variable {F : Type u} [Field F] (j : F)
 
 private lemma two_or_three_ne_zero : (2 : F) ≠ 0 ∨ (3 : F) ≠ 0 :=
-  ne_zero_or_ne_zero_of_nat_coprime (show Nat.coprime 2 3 by norm_num1)
+  ne_zero_or_ne_zero_of_nat_coprime (show Nat.Coprime 2 3 by norm_num1)
 
 variable [DecidableEq F]
 
diff --git a/Mathlib/Data/Int/GCD.lean b/Mathlib/Data/Int/GCD.lean
index f524cf6c55d3d..741d974c9c0cd 100644
--- a/Mathlib/Data/Int/GCD.lean
+++ b/Mathlib/Data/Int/GCD.lean
@@ -167,7 +167,7 @@ theorem exists_mul_emod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m, n * m % k
     ← Int.mul_emod]
 #align nat.exists_mul_mod_eq_gcd Nat.exists_mul_emod_eq_gcd
 
-theorem exists_mul_emod_eq_one_of_coprime {k n : ℕ} (hkn : coprime n k) (hk : 1 < k) :
+theorem exists_mul_emod_eq_one_of_coprime {k n : ℕ} (hkn : Coprime n k) (hk : 1 < k) :
     ∃ m, n * m % k = 1 :=
   Exists.recOn (exists_mul_emod_eq_gcd (lt_of_le_of_lt (le_of_eq hkn) hk)) fun m hm ↦
     ⟨m, hm.trans hkn⟩
diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
index 50c0179204317..a446a520cd44c 100644
--- a/Mathlib/Data/Int/ModEq.lean
+++ b/Mathlib/Data/Int/ModEq.lean
@@ -264,7 +264,7 @@ theorem add_modEq_left : n + a ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <
 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) :
+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
     rw [modEq_iff_dvd, modEq_iff_dvd] at h
@@ -294,9 +294,9 @@ theorem modEq_add_fac_self {a t n : ℤ} : a + n * t ≡ a [ZMOD n] :=
   modEq_add_fac _ ModEq.rfl
 #align int.modeq_add_fac_self Int.modEq_add_fac_self
 
-theorem mod_coprime {a b : ℕ} (hab : Nat.coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
+theorem mod_coprime {a b : ℕ} (hab : Nat.Coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
   ⟨Nat.gcdA a b,
-    have hgcd : Nat.gcd a b = 1 := Nat.coprime.gcd_eq_one hab
+    have hgcd : Nat.gcd a b = 1 := Nat.Coprime.gcd_eq_one hab
     calc
       ↑a * Nat.gcdA a b ≡ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b [ZMOD ↑b] :=
         ModEq.symm <| modEq_add_fac _ <| ModEq.refl _
diff --git a/Mathlib/Data/Nat/Choose/Central.lean b/Mathlib/Data/Nat/Choose/Central.lean
index 796fa79186b09..95b68c78116e8 100644
--- a/Mathlib/Data/Nat/Choose/Central.lean
+++ b/Mathlib/Data/Nat/Choose/Central.lean
@@ -129,7 +129,7 @@ theorem two_dvd_centralBinom_of_one_le {n : ℕ} (h : 0 < n) : 2 ∣ centralBino
 /-- A crucial lemma to ensure that Catalan numbers can be defined via their explicit formula
   `catalan n = n.centralBinom / (n + 1)`. -/
 theorem succ_dvd_centralBinom (n : ℕ) : n + 1 ∣ n.centralBinom := by
-  have h_s : (n + 1).coprime (2 * n + 1) := by
+  have h_s : (n + 1).Coprime (2 * n + 1) := by
     rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
     exact coprime_one_left n
   apply h_s.dvd_of_dvd_mul_left
diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
index f76683c5ca2e6..2767e90f2aa14 100644
--- a/Mathlib/Data/Nat/Factorization/Basic.lean
+++ b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -528,7 +528,7 @@ theorem not_dvd_ord_compl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : ¬p ∣ or
   simp [hp.factorization]
 #align nat.not_dvd_ord_compl Nat.not_dvd_ord_compl
 
-theorem coprime_ord_compl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : coprime p (ord_compl[p] n) :=
+theorem coprime_ord_compl {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) : Coprime p (ord_compl[p] n) :=
   (or_iff_left (not_dvd_ord_compl hp hn)).mp <| coprime_or_dvd_of_prime hp _
 #align nat.coprime_ord_compl Nat.coprime_ord_compl
 
@@ -743,13 +743,13 @@ theorem Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb :
 
 
 /-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
-theorem factorization_mul_apply_of_coprime {p a b : ℕ} (hab : coprime a b) :
+theorem factorization_mul_apply_of_coprime {p a b : ℕ} (hab : Coprime a b) :
     (a * b).factorization p = a.factorization p + b.factorization p := by
   simp only [← factors_count_eq, perm_iff_count.mp (perm_factors_mul_of_coprime hab), count_append]
 #align nat.factorization_mul_apply_of_coprime Nat.factorization_mul_apply_of_coprime
 
 /-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
-theorem factorization_mul_of_coprime {a b : ℕ} (hab : coprime a b) :
+theorem factorization_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
     (a * b).factorization = a.factorization + b.factorization := by
   ext q
   rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]
@@ -757,7 +757,7 @@ theorem factorization_mul_of_coprime {a b : ℕ} (hab : coprime a b) :
 
 /-- If `p` is a prime factor of `a` then the power of `p` in `a` is the same that in `a * b`,
 for any `b` coprime to `a`. -/
-theorem factorization_eq_of_coprime_left {p a b : ℕ} (hab : coprime a b) (hpa : p ∈ a.factors) :
+theorem factorization_eq_of_coprime_left {p a b : ℕ} (hab : Coprime a b) (hpa : p ∈ a.factors) :
     (a * b).factorization p = a.factorization p := by
   rw [factorization_mul_apply_of_coprime hab, ← factors_count_eq, ← factors_count_eq,
     count_eq_zero_of_not_mem (coprime_factors_disjoint hab hpa), add_zero]
@@ -765,21 +765,21 @@ theorem factorization_eq_of_coprime_left {p a b : ℕ} (hab : coprime a b) (hpa
 
 /-- If `p` is a prime factor of `b` then the power of `p` in `b` is the same that in `a * b`,
 for any `a` coprime to `b`. -/
-theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : coprime a b) (hpb : p ∈ b.factors) :
+theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : Coprime a b) (hpb : p ∈ b.factors) :
     (a * b).factorization p = b.factorization p := by
   rw [mul_comm]
   exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb
 #align nat.factorization_eq_of_coprime_right Nat.factorization_eq_of_coprime_right
 
 /-- The prime factorizations of coprime `a` and `b` are disjoint -/
-theorem factorization_disjoint_of_coprime {a b : ℕ} (hab : coprime a b) :
+theorem factorization_disjoint_of_coprime {a b : ℕ} (hab : Coprime a b) :
     Disjoint a.factorization.support b.factorization.support := by
   simpa only [support_factorization] using
     disjoint_toFinset_iff_disjoint.mpr (coprime_factors_disjoint hab)
 #align nat.factorization_disjoint_of_coprime Nat.factorization_disjoint_of_coprime
 
 /-- For coprime `a` and `b` the prime factorization `a * b` is the union of those of `a` and `b` -/
-theorem factorization_mul_support_of_coprime {a b : ℕ} (hab : coprime a b) :
+theorem factorization_mul_support_of_coprime {a b : ℕ} (hab : Coprime a b) :
     (a * b).factorization.support = a.factorization.support ∪ b.factorization.support := by
   rw [factorization_mul_of_coprime hab]
   exact support_add_eq (factorization_disjoint_of_coprime hab)
@@ -827,7 +827,7 @@ def recOnPrimePow {P : ℕ → Sort*} (h0 : P 0) (h1 : P 1)
 `P b` to `P (a * b)` when `a, b` are positive coprime, we can define `P` for all natural numbers. -/
 @[elab_as_elim]
 def recOnPosPrimePosCoprime {P : ℕ → Sort*} (hp : ∀ p n : ℕ, Prime p → 0 < n → P (p ^ n))
-    (h0 : P 0) (h1 : P 1) (h : ∀ a b, 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)) :
+    (h0 : P 0) (h1 : P 1) (h : ∀ a b, 1 < a → 1 < b → Coprime a b → P a → P b → P (a * b)) :
     ∀ a, P a :=
   recOnPrimePow h0 h1 <| by
     intro a p n hp' hpa hn hPa
@@ -844,7 +844,7 @@ def recOnPosPrimePosCoprime {P : ℕ → Sort*} (hp : ∀ p n : ℕ, Prime p →
 `P (a * b)` when `a, b` are positive coprime, we can define `P` for all natural numbers. -/
 @[elab_as_elim]
 def recOnPrimeCoprime {P : ℕ → Sort*} (h0 : P 0) (hp : ∀ p n : ℕ, Prime p → P (p ^ n))
-    (h : ∀ a b, 1 < a → 1 < b → coprime a b → P a → P b → P (a * b)) : ∀ a, P a :=
+    (h : ∀ a b, 1 < a → 1 < b → Coprime a b → P a → P b → P (a * b)) : ∀ a, P a :=
   recOnPosPrimePosCoprime (fun p n h _ => hp p n h) h0 (hp 2 0 prime_two) h
 #align nat.rec_on_prime_coprime Nat.recOnPrimeCoprime
 
@@ -865,7 +865,7 @@ noncomputable def recOnMul {P : ℕ → Sort*} (h0 : P 0) (h1 : P 1) (hp : ∀ p
 /-- For any multiplicative function `f` with `f 1 = 1` and any `n ≠ 0`,
 we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n` -/
 theorem multiplicative_factorization {β : Type*} [CommMonoid β] (f : ℕ → β)
-    (h_mult : ∀ x y : ℕ, coprime x y → f (x * y) = f x * f y) (hf : f 1 = 1) :
+    (h_mult : ∀ x y : ℕ, Coprime x y → f (x * y) = f x * f y) (hf : f 1 = 1) :
     ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k) := by
   apply Nat.recOnPosPrimePosCoprime
   · rintro p k hp - -
@@ -885,7 +885,7 @@ theorem multiplicative_factorization {β : Type*} [CommMonoid β] (f : ℕ → 
 /-- For any multiplicative function `f` with `f 1 = 1` and `f 0 = 1`,
 we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n` -/
 theorem multiplicative_factorization' {β : Type*} [CommMonoid β] (f : ℕ → β)
-    (h_mult : ∀ x y : ℕ, coprime x y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) :
+    (h_mult : ∀ x y : ℕ, Coprime x y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) :
     ∀ {n : ℕ}, f n = n.factorization.prod fun p k => f (p ^ k) := by
   apply Nat.recOnPosPrimePosCoprime
   · rintro p k hp -
diff --git a/Mathlib/Data/Nat/Factorization/PrimePow.lean b/Mathlib/Data/Nat/Factorization/PrimePow.lean
index 1410e1d7515e1..542eef569f8f0 100644
--- a/Mathlib/Data/Nat/Factorization/PrimePow.lean
+++ b/Mathlib/Data/Nat/Factorization/PrimePow.lean
@@ -117,7 +117,7 @@ theorem isPrimePow_pow_iff {n k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) ↔ I
   exact ⟨hp.dvd_of_dvd_pow, fun t => t.trans (dvd_pow_self _ hk)⟩
 #align is_prime_pow_pow_iff isPrimePow_pow_iff
 
-theorem Nat.coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.coprime a b) (hn : IsPrimePow n) :
+theorem Nat.Coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.Coprime a b) (hn : IsPrimePow n) :
     n ∣ a * b ↔ n ∣ a ∨ n ∣ b := by
   rcases eq_or_ne a 0 with (rfl | ha)
   · simp only [Nat.coprime_zero_left] at hab
@@ -139,9 +139,9 @@ theorem Nat.coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.coprime a b) (hn
     intro t -- porting note: used to be `exact` below, but the definition of `∈` has changed.
     simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
   cases' this with h h <;> simp [h, imp_or]
-#align nat.coprime.is_prime_pow_dvd_mul Nat.coprime.isPrimePow_dvd_mul
+#align nat.coprime.is_prime_pow_dvd_mul Nat.Coprime.isPrimePow_dvd_mul
 
-theorem Nat.mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.coprime b) :
+theorem Nat.mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.Coprime b) :
     (a * b).divisors.filter IsPrimePow = (a.divisors ∪ b.divisors).filter IsPrimePow := by
   rcases eq_or_ne a 0 with (rfl | ha)
   · simp only [Nat.coprime_zero_left] at hab
diff --git a/Mathlib/Data/Nat/Factors.lean b/Mathlib/Data/Nat/Factors.lean
index b5372f2b06dda..2314cde4a5bf7 100644
--- a/Mathlib/Data/Nat/Factors.lean
+++ b/Mathlib/Data/Nat/Factors.lean
@@ -203,7 +203,7 @@ theorem perm_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
 #align nat.perm_factors_mul Nat.perm_factors_mul
 
 /-- For coprime `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b` -/
-theorem perm_factors_mul_of_coprime {a b : ℕ} (hab : coprime a b) :
+theorem perm_factors_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
     (a * b).factors ~ a.factors ++ b.factors := by
   rcases a.eq_zero_or_pos with (rfl | ha)
   · simp [(coprime_zero_left _).mp hab]
@@ -257,7 +257,7 @@ theorem mem_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} :
 #align nat.mem_factors_mul Nat.mem_factors_mul
 
 /-- The sets of factors of coprime `a` and `b` are disjoint -/
-theorem coprime_factors_disjoint {a b : ℕ} (hab : a.coprime b) :
+theorem coprime_factors_disjoint {a b : ℕ} (hab : a.Coprime b) :
     List.Disjoint a.factors b.factors := by
   intro q hqa hqb
   apply not_prime_one
@@ -265,7 +265,7 @@ theorem coprime_factors_disjoint {a b : ℕ} (hab : a.coprime b) :
   exact prime_of_mem_factors hqa
 #align nat.coprime_factors_disjoint Nat.coprime_factors_disjoint
 
-theorem mem_factors_mul_of_coprime {a b : ℕ} (hab : coprime a b) (p : ℕ) :
+theorem mem_factors_mul_of_coprime {a b : ℕ} (hab : Coprime a b) (p : ℕ) :
     p ∈ (a * b).factors ↔ p ∈ a.factors ∪ b.factors := by
   rcases a.eq_zero_or_pos with (rfl | ha)
   · simp [(coprime_zero_left _).mp hab]
diff --git a/Mathlib/Data/Nat/Fib.lean b/Mathlib/Data/Nat/Fib.lean
index 50020ebe49c8b..c091df4e47964 100644
--- a/Mathlib/Data/Nat/Fib.lean
+++ b/Mathlib/Data/Nat/Fib.lean
@@ -135,12 +135,12 @@ theorem le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n := by
 
 /-- Subsequent Fibonacci numbers are coprime,
   see https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime -/
-theorem fib_coprime_fib_succ (n : ℕ) : Nat.coprime (fib n) (fib (n + 1)) := by
+theorem fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (fib n) (fib (n + 1)) := by
   induction' n with n ih
   · simp
   · rw [fib_add_two]
     simp only [coprime_add_self_right]
-    simp [coprime, ih.symm]
+    simp [Coprime, ih.symm]
 #align nat.fib_coprime_fib_succ Nat.fib_coprime_fib_succ
 
 /-- See https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers -/
@@ -258,7 +258,7 @@ theorem gcd_fib_add_self (m n : ℕ) : gcd (fib m) (fib (n + m)) = gcd (fib m) (
     _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
         rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
     _ = gcd (fib m) (fib (n.pred + 1)) :=
-      coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (coprime.symm (fib_coprime_fib_succ m))
+      Coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (Coprime.symm (fib_coprime_fib_succ m))
 #align nat.gcd_fib_add_self Nat.gcd_fib_add_self
 
 theorem gcd_fib_add_mul_self (m n : ℕ) : ∀ k, gcd (fib m) (fib (n + k * m)) = gcd (fib m) (fib n)
diff --git a/Mathlib/Data/Nat/GCD/Basic.lean b/Mathlib/Data/Nat/GCD/Basic.lean
index 6946528654936..b44525fae9d75 100644
--- a/Mathlib/Data/Nat/GCD/Basic.lean
+++ b/Mathlib/Data/Nat/GCD/Basic.lean
@@ -129,107 +129,107 @@ theorem lcm_pos {m n : ℕ} : 0 < m → 0 < n → 0 < m.lcm n := by
 #align nat.lcm_pos Nat.lcm_pos
 
 /-!
-### `coprime`
+### `Coprime`
 
-See also `Nat.coprime_of_dvd` and `Nat.coprime_of_dvd'` to prove `Nat.coprime m n`.
+See also `Nat.coprime_of_dvd` and `Nat.coprime_of_dvd'` to prove `Nat.Coprime m n`.
 -/
 
-instance (m n : ℕ) : Decidable (coprime m n) := inferInstanceAs (Decidable (gcd m n = 1))
+instance (m n : ℕ) : Decidable (Coprime m n) := inferInstanceAs (Decidable (gcd m n = 1))
 
-theorem coprime.lcm_eq_mul {m n : ℕ} (h : coprime m n) : lcm m n = m * n := by
+theorem Coprime.lcm_eq_mul {m n : ℕ} (h : Coprime m n) : lcm m n = m * n := by
   rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
-#align nat.coprime.lcm_eq_mul Nat.coprime.lcm_eq_mul
+#align nat.coprime.lcm_eq_mul Nat.Coprime.lcm_eq_mul
 
-theorem coprime.symmetric : Symmetric coprime := fun _ _ => coprime.symm
-#align nat.coprime.symmetric Nat.coprime.symmetric
+theorem Coprime.symmetric : Symmetric Coprime := fun _ _ => Coprime.symm
+#align nat.coprime.symmetric Nat.Coprime.symmetric
 
-theorem coprime.dvd_mul_right {m n k : ℕ} (H : coprime k n) : k ∣ m * n ↔ k ∣ m :=
+theorem Coprime.dvd_mul_right {m n k : ℕ} (H : Coprime k n) : k ∣ m * n ↔ k ∣ m :=
   ⟨H.dvd_of_dvd_mul_right, fun h => dvd_mul_of_dvd_left h n⟩
-#align nat.coprime.dvd_mul_right Nat.coprime.dvd_mul_right
+#align nat.coprime.dvd_mul_right Nat.Coprime.dvd_mul_right
 
-theorem coprime.dvd_mul_left {m n k : ℕ} (H : coprime k m) : k ∣ m * n ↔ k ∣ n :=
+theorem Coprime.dvd_mul_left {m n k : ℕ} (H : Coprime k m) : k ∣ m * n ↔ k ∣ n :=
   ⟨H.dvd_of_dvd_mul_left, fun h => dvd_mul_of_dvd_right h m⟩
-#align nat.coprime.dvd_mul_left Nat.coprime.dvd_mul_left
+#align nat.coprime.dvd_mul_left Nat.Coprime.dvd_mul_left
 
 @[simp]
-theorem coprime_add_self_right {m n : ℕ} : coprime m (n + m) ↔ coprime m n := by
-  rw [coprime, coprime, gcd_add_self_right]
+theorem coprime_add_self_right {m n : ℕ} : Coprime m (n + m) ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_add_self_right]
 #align nat.coprime_add_self_right Nat.coprime_add_self_right
 
 @[simp]
-theorem coprime_self_add_right {m n : ℕ} : coprime m (m + n) ↔ coprime m n := by
+theorem coprime_self_add_right {m n : ℕ} : Coprime m (m + n) ↔ Coprime m n := by
   rw [add_comm, coprime_add_self_right]
 #align nat.coprime_self_add_right Nat.coprime_self_add_right
 
 @[simp]
-theorem coprime_add_self_left {m n : ℕ} : coprime (m + n) n ↔ coprime m n := by
-  rw [coprime, coprime, gcd_add_self_left]
+theorem coprime_add_self_left {m n : ℕ} : Coprime (m + n) n ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_add_self_left]
 #align nat.coprime_add_self_left Nat.coprime_add_self_left
 
 @[simp]
-theorem coprime_self_add_left {m n : ℕ} : coprime (m + n) m ↔ coprime n m := by
-  rw [coprime, coprime, gcd_self_add_left]
+theorem coprime_self_add_left {m n : ℕ} : Coprime (m + n) m ↔ Coprime n m := by
+  rw [Coprime, Coprime, gcd_self_add_left]
 #align nat.coprime_self_add_left Nat.coprime_self_add_left
 
 @[simp]
-theorem coprime_add_mul_right_right (m n k : ℕ) : coprime m (n + k * m) ↔ coprime m n := by
-  rw [coprime, coprime, gcd_add_mul_right_right]
+theorem coprime_add_mul_right_right (m n k : ℕ) : Coprime m (n + k * m) ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_add_mul_right_right]
 #align nat.coprime_add_mul_right_right Nat.coprime_add_mul_right_right
 
 @[simp]
-theorem coprime_add_mul_left_right (m n k : ℕ) : coprime m (n + m * k) ↔ coprime m n := by
-  rw [coprime, coprime, gcd_add_mul_left_right]
+theorem coprime_add_mul_left_right (m n k : ℕ) : Coprime m (n + m * k) ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_add_mul_left_right]
 #align nat.coprime_add_mul_left_right Nat.coprime_add_mul_left_right
 
 @[simp]
-theorem coprime_mul_right_add_right (m n k : ℕ) : coprime m (k * m + n) ↔ coprime m n := by
-  rw [coprime, coprime, gcd_mul_right_add_right]
+theorem coprime_mul_right_add_right (m n k : ℕ) : Coprime m (k * m + n) ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_mul_right_add_right]
 #align nat.coprime_mul_right_add_right Nat.coprime_mul_right_add_right
 
 @[simp]
-theorem coprime_mul_left_add_right (m n k : ℕ) : coprime m (m * k + n) ↔ coprime m n := by
-  rw [coprime, coprime, gcd_mul_left_add_right]
+theorem coprime_mul_left_add_right (m n k : ℕ) : Coprime m (m * k + n) ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_mul_left_add_right]
 #align nat.coprime_mul_left_add_right Nat.coprime_mul_left_add_right
 
 @[simp]
-theorem coprime_add_mul_right_left (m n k : ℕ) : coprime (m + k * n) n ↔ coprime m n := by
-  rw [coprime, coprime, gcd_add_mul_right_left]
+theorem coprime_add_mul_right_left (m n k : ℕ) : Coprime (m + k * n) n ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_add_mul_right_left]
 #align nat.coprime_add_mul_right_left Nat.coprime_add_mul_right_left
 
 @[simp]
-theorem coprime_add_mul_left_left (m n k : ℕ) : coprime (m + n * k) n ↔ coprime m n := by
-  rw [coprime, coprime, gcd_add_mul_left_left]
+theorem coprime_add_mul_left_left (m n k : ℕ) : Coprime (m + n * k) n ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_add_mul_left_left]
 #align nat.coprime_add_mul_left_left Nat.coprime_add_mul_left_left
 
 @[simp]
-theorem coprime_mul_right_add_left (m n k : ℕ) : coprime (k * n + m) n ↔ coprime m n := by
-  rw [coprime, coprime, gcd_mul_right_add_left]
+theorem coprime_mul_right_add_left (m n k : ℕ) : Coprime (k * n + m) n ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_mul_right_add_left]
 #align nat.coprime_mul_right_add_left Nat.coprime_mul_right_add_left
 
 @[simp]
-theorem coprime_mul_left_add_left (m n k : ℕ) : coprime (n * k + m) n ↔ coprime m n := by
-  rw [coprime, coprime, gcd_mul_left_add_left]
+theorem coprime_mul_left_add_left (m n k : ℕ) : Coprime (n * k + m) n ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_mul_left_add_left]
 #align nat.coprime_mul_left_add_left Nat.coprime_mul_left_add_left
 
 @[simp]
-theorem coprime_sub_self_left {m n : ℕ} (h : m ≤ n) : coprime (n - m) m ↔ coprime n m := by
-  rw [coprime, coprime, gcd_sub_self_left h]
+theorem coprime_sub_self_left {m n : ℕ} (h : m ≤ n) : Coprime (n - m) m ↔ Coprime n m := by
+  rw [Coprime, Coprime, gcd_sub_self_left h]
 
 @[simp]
-theorem coprime_sub_self_right {m n : ℕ} (h : m ≤ n) : coprime m (n - m) ↔ coprime m n:= by
-  rw [coprime, coprime, gcd_sub_self_right h]
+theorem coprime_sub_self_right {m n : ℕ} (h : m ≤ n) : Coprime m (n - m) ↔ Coprime m n:= by
+  rw [Coprime, Coprime, gcd_sub_self_right h]
 
 @[simp]
-theorem coprime_self_sub_left {m n : ℕ} (h : m ≤ n) : coprime (n - m) n ↔ coprime m n := by
-  rw [coprime, coprime, gcd_self_sub_left h]
+theorem coprime_self_sub_left {m n : ℕ} (h : m ≤ n) : Coprime (n - m) n ↔ Coprime m n := by
+  rw [Coprime, Coprime, gcd_self_sub_left h]
 
 @[simp]
-theorem coprime_self_sub_right {m n : ℕ} (h : m ≤ n) : coprime n (n - m) ↔ coprime n m := by
-  rw [coprime, coprime, gcd_self_sub_right h]
+theorem coprime_self_sub_right {m n : ℕ} (h : m ≤ n) : Coprime n (n - m) ↔ Coprime n m := by
+  rw [Coprime, Coprime, gcd_self_sub_right h]
 
 @[simp]
 theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
-    Nat.coprime (a ^ n) b ↔ Nat.coprime a b := by
+    Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b := by
   obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero hn.ne'
   rw [pow_succ, Nat.coprime_mul_iff_left]
   exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩
@@ -237,33 +237,33 @@ theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
 
 @[simp]
 theorem coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
-    Nat.coprime a (b ^ n) ↔ Nat.coprime a b := by
+    Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b := by
   rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
 #align nat.coprime_pow_right_iff Nat.coprime_pow_right_iff
 
-theorem not_coprime_zero_zero : ¬coprime 0 0 := by simp
+theorem not_coprime_zero_zero : ¬Coprime 0 0 := by simp
 #align nat.not_coprime_zero_zero Nat.not_coprime_zero_zero
 
-theorem coprime_one_left_iff (n : ℕ) : coprime 1 n ↔ True := by simp [coprime]
+theorem coprime_one_left_iff (n : ℕ) : Coprime 1 n ↔ True := by simp [Coprime]
 #align nat.coprime_one_left_iff Nat.coprime_one_left_iff
 
-theorem coprime_one_right_iff (n : ℕ) : coprime n 1 ↔ True := by simp [coprime]
+theorem coprime_one_right_iff (n : ℕ) : Coprime n 1 ↔ True := by simp [Coprime]
 #align nat.coprime_one_right_iff Nat.coprime_one_right_iff
 
-theorem gcd_mul_of_coprime_of_dvd {a b c : ℕ} (hac : coprime a c) (b_dvd_c : b ∣ c) :
+theorem gcd_mul_of_coprime_of_dvd {a b c : ℕ} (hac : Coprime a c) (b_dvd_c : b ∣ c) :
     gcd (a * b) c = b := by
   rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
   rw [gcd_mul_right]
   convert one_mul b
-  exact coprime.coprime_mul_right_right hac
+  exact Coprime.coprime_mul_right_right hac
 #align nat.gcd_mul_of_coprime_of_dvd Nat.gcd_mul_of_coprime_of_dvd
 
-theorem coprime.eq_of_mul_eq_zero {m n : ℕ} (h : m.coprime n) (hmn : m * n = 0) :
+theorem Coprime.eq_of_mul_eq_zero {m n : ℕ} (h : m.Coprime n) (hmn : m * n = 0) :
     m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0 :=
   (Nat.eq_zero_of_mul_eq_zero hmn).imp (fun hm => ⟨hm, n.coprime_zero_left.mp <| hm ▸ h⟩) fun hn =>
     let eq := hn ▸ h.symm
     ⟨m.coprime_zero_left.mp <| eq, hn⟩
-#align nat.coprime.eq_of_mul_eq_zero Nat.coprime.eq_of_mul_eq_zero
+#align nat.coprime.eq_of_mul_eq_zero Nat.Coprime.eq_of_mul_eq_zero
 
 /-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`.
 
@@ -307,7 +307,7 @@ theorem pow_dvd_pow_iff {a b n : ℕ} (n0 : 0 < n) : a ^ n ∣ b ^ n ↔ a ∣ b
 #align nat.pow_dvd_pow_iff Nat.pow_dvd_pow_iff
 
 /-- If `k:ℕ` divides coprime `a` and `b` then `k = 1` -/
-theorem eq_one_of_dvd_coprimes {a b k : ℕ} (h_ab_coprime : coprime a b) (hka : k ∣ a)
+theorem eq_one_of_dvd_coprimes {a b k : ℕ} (h_ab_coprime : Coprime a b) (hka : k ∣ a)
     (hkb : k ∣ b) : k = 1 := by
   rw [coprime_iff_gcd_eq_one] at h_ab_coprime
   have h1 := dvd_gcd hka hkb
@@ -315,7 +315,7 @@ theorem eq_one_of_dvd_coprimes {a b k : ℕ} (h_ab_coprime : coprime a b) (hka :
   exact Nat.dvd_one.mp h1
 #align nat.eq_one_of_dvd_coprimes Nat.eq_one_of_dvd_coprimes
 
-theorem coprime.mul_add_mul_ne_mul {m n a b : ℕ} (cop : coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) :
+theorem Coprime.mul_add_mul_ne_mul {m n a b : ℕ} (cop : Coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) :
     a * m + b * n ≠ m * n := by
   intro h
   obtain ⟨x, rfl⟩ : n ∣ a :=
@@ -329,6 +329,6 @@ theorem coprime.mul_add_mul_ne_mul {m n a b : ℕ} (cop : coprime m n) (ha : a 
   rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
   refine' mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) _)
   rw [← mul_assoc, ← h, add_mul, add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
-#align nat.coprime.mul_add_mul_ne_mul Nat.coprime.mul_add_mul_ne_mul
+#align nat.coprime.mul_add_mul_ne_mul Nat.Coprime.mul_add_mul_ne_mul
 
 end Nat
diff --git a/Mathlib/Data/Nat/GCD/BigOperators.lean b/Mathlib/Data/Nat/GCD/BigOperators.lean
index fb84079ef3f8c..efb5812d79abd 100644
--- a/Mathlib/Data/Nat/GCD/BigOperators.lean
+++ b/Mathlib/Data/Nat/GCD/BigOperators.lean
@@ -20,14 +20,14 @@ open BigOperators
 
 /-- See `IsCoprime.prod_left` for the corresponding lemma about `IsCoprime` -/
 theorem coprime_prod_left {ι : Type*} {x : ℕ} {s : ι → ℕ} {t : Finset ι} :
-    (∀ i : ι, i ∈ t → coprime (s i) x) → coprime (∏ i : ι in t, s i) x :=
-  Finset.prod_induction s (fun y ↦ y.coprime x) (fun a b ↦ coprime.mul) (by simp)
+    (∀ i : ι, i ∈ t → Coprime (s i) x) → Coprime (∏ i : ι in t, s i) x :=
+  Finset.prod_induction s (fun y ↦ y.Coprime x) (fun a b ↦ Coprime.mul) (by simp)
 #align nat.coprime_prod_left Nat.coprime_prod_left
 
 /-- See `IsCoprime.prod_right` for the corresponding lemma about `IsCoprime` -/
 theorem coprime_prod_right {ι : Type*} {x : ℕ} {s : ι → ℕ} {t : Finset ι} :
-    (∀ i : ι, i ∈ t → coprime x (s i)) → coprime x (∏ i : ι in t, s i) :=
-  Finset.prod_induction s (fun y ↦ x.coprime y) (fun a b ↦ coprime.mul_right) (by simp)
+    (∀ i : ι, i ∈ t → Coprime x (s i)) → Coprime x (∏ i : ι in t, s i) :=
+  Finset.prod_induction s (fun y ↦ x.Coprime y) (fun a b ↦ Coprime.mul_right) (by simp)
 #align nat.coprime_prod_right Nat.coprime_prod_right
 
 end Nat
diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean
index f0c05a787a110..9aefe98f4bd93 100644
--- a/Mathlib/Data/Nat/ModEq.lean
+++ b/Mathlib/Data/Nat/ModEq.lean
@@ -365,7 +365,7 @@ def chineseRemainder' (h : a ≡ b [MOD gcd n m]) : { k // k ≡ a [MOD n] ∧ k
 #align nat.chinese_remainder' Nat.chineseRemainder'
 
 /-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m` -/
-def chineseRemainder (co : n.coprime m) (a b : ℕ) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] } :=
+def chineseRemainder (co : n.Coprime m) (a b : ℕ) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] } :=
   chineseRemainder' (by convert @modEq_one a b)
 #align nat.chinese_remainder Nat.chineseRemainder
 
@@ -377,12 +377,12 @@ theorem chineseRemainder'_lt_lcm (h : a ≡ b [MOD gcd n m]) (hn : n ≠ 0) (hm
   exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)
 #align nat.chinese_remainder'_lt_lcm Nat.chineseRemainder'_lt_lcm
 
-theorem chineseRemainder_lt_mul (co : n.coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) :
+theorem chineseRemainder_lt_mul (co : n.Coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) :
     ↑(chineseRemainder co a b) < n * m :=
   lt_of_lt_of_le (chineseRemainder'_lt_lcm _ hn hm) (le_of_eq co.lcm_eq_mul)
 #align nat.chinese_remainder_lt_mul Nat.chineseRemainder_lt_mul
 
-theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.coprime n) :
+theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.Coprime n) :
     a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n] :=
   ⟨fun h => by
     rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs,
@@ -392,7 +392,7 @@ theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.coprime n) :
     ⟨h.of_mul_right _, h.of_mul_left _⟩⟩
 #align nat.modeq_and_modeq_iff_modeq_mul Nat.modEq_and_modEq_iff_modEq_mul
 
-theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.coprime n := by
+theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n := by
   obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
   rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
   calc
diff --git a/Mathlib/Data/Nat/Periodic.lean b/Mathlib/Data/Nat/Periodic.lean
index 7442c5cc17b4a..ab9d965291b46 100644
--- a/Mathlib/Data/Nat/Periodic.lean
+++ b/Mathlib/Data/Nat/Periodic.lean
@@ -25,7 +25,7 @@ theorem periodic_gcd (a : ℕ) : Periodic (gcd a) a := by
   simp only [forall_const, gcd_add_self_right, eq_self_iff_true, Periodic]
 #align nat.periodic_gcd Nat.periodic_gcd
 
-theorem periodic_coprime (a : ℕ) : Periodic (coprime a) a := by
+theorem periodic_coprime (a : ℕ) : Periodic (Coprime a) a := by
   simp only [coprime_add_self_right, forall_const, iff_self_iff, eq_iff_iff, Periodic]
 #align nat.periodic_coprime Nat.periodic_coprime
 
diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean
index 1fe1c9b9e5e0b..383edd071c8ae 100644
--- a/Mathlib/Data/Nat/Prime.lean
+++ b/Mathlib/Data/Nat/Prime.lean
@@ -143,7 +143,7 @@ theorem prime_def_le_sqrt {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, 2 ≤ m →
           rwa [one_mul, ← e]⟩
 #align nat.prime_def_le_sqrt Nat.prime_def_le_sqrt
 
-theorem prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.coprime m) : Prime n := by
+theorem prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.Coprime m) : Prime n := by
   refine' prime_def_lt.mpr ⟨h1, fun m mlt mdvd => _⟩
   have hm : m ≠ 0 := by
     rintro rfl
@@ -517,7 +517,7 @@ theorem Prime.mod_two_eq_one_iff_ne_two {p : ℕ} [Fact p.Prime] : p % 2 = 1 ↔
   simp at h
 #align nat.prime.mod_two_eq_one_iff_ne_two Nat.Prime.mod_two_eq_one_iff_ne_two
 
-theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → ¬k ∣ n) : coprime m n := by
+theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → ¬k ∣ n) : Coprime m n := by
   rw [coprime_iff_gcd_eq_one]
   by_contra g2
   obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
@@ -526,7 +526,7 @@ theorem coprime_of_dvd {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → ¬k ∣ n
   · exact gcd_dvd_right _ _
 #align nat.coprime_of_dvd Nat.coprime_of_dvd
 
-theorem coprime_of_dvd' {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → k ∣ n → k ∣ 1) : coprime m n :=
+theorem coprime_of_dvd' {m n : ℕ} (H : ∀ k, Prime k → k ∣ m → k ∣ n → k ∣ 1) : Coprime m n :=
   coprime_of_dvd fun k kp km kn => not_le_of_gt kp.one_lt <| le_of_dvd zero_lt_one <| H k kp km kn
 #align nat.coprime_of_dvd' Nat.coprime_of_dvd'
 
@@ -538,16 +538,16 @@ theorem factors_lemma {k} : (k + 2) / minFac (k + 2) < k + 2 :=
       )).one_lt
 #align nat.factors_lemma Nat.factors_lemma
 
-theorem Prime.coprime_iff_not_dvd {p n : ℕ} (pp : Prime p) : coprime p n ↔ ¬p ∣ n :=
+theorem Prime.coprime_iff_not_dvd {p n : ℕ} (pp : Prime p) : Coprime p n ↔ ¬p ∣ n :=
   ⟨fun co d => pp.not_dvd_one <| co.dvd_of_dvd_mul_left (by simp [d]), fun nd =>
     coprime_of_dvd fun m m2 mp => ((prime_dvd_prime_iff_eq m2 pp).1 mp).symm ▸ nd⟩
 #align nat.prime.coprime_iff_not_dvd Nat.Prime.coprime_iff_not_dvd
 
-theorem Prime.dvd_iff_not_coprime {p n : ℕ} (pp : Prime p) : p ∣ n ↔ ¬coprime p n :=
+theorem Prime.dvd_iff_not_coprime {p n : ℕ} (pp : Prime p) : p ∣ n ↔ ¬Coprime p n :=
   iff_not_comm.2 pp.coprime_iff_not_dvd
 #align nat.prime.dvd_iff_not_coprime Nat.Prime.dvd_iff_not_coprime
 
-theorem Prime.not_coprime_iff_dvd {m n : ℕ} : ¬coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n := by
+theorem Prime.not_coprime_iff_dvd {m n : ℕ} : ¬Coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n := by
   apply Iff.intro
   · intro h
     exact
@@ -664,29 +664,29 @@ theorem Prime.dvd_factorial : ∀ {n p : ℕ} (_ : Prime p), p ∣ n ! ↔ p ≤
         (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
 #align nat.prime.dvd_factorial Nat.Prime.dvd_factorial
 
-theorem Prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : coprime a (p ^ m) :=
+theorem Prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) : Coprime a (p ^ m) :=
   (pp.coprime_iff_not_dvd.2 h).symm.pow_right _
 #align nat.prime.coprime_pow_of_not_dvd Nat.Prime.coprime_pow_of_not_dvd
 
-theorem coprime_primes {p q : ℕ} (pp : Prime p) (pq : Prime q) : coprime p q ↔ p ≠ q :=
+theorem coprime_primes {p q : ℕ} (pp : Prime p) (pq : Prime q) : Coprime p q ↔ p ≠ q :=
   pp.coprime_iff_not_dvd.trans <| not_congr <| dvd_prime_two_le pq pp.two_le
 #align nat.coprime_primes Nat.coprime_primes
 
 theorem coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : Prime p) (pq : Prime q) (h : p ≠ q) :
-    coprime (p ^ n) (q ^ m) :=
+    Coprime (p ^ n) (q ^ m) :=
   ((coprime_primes pp pq).2 h).pow _ _
 #align nat.coprime_pow_primes Nat.coprime_pow_primes
 
-theorem coprime_or_dvd_of_prime {p} (pp : Prime p) (i : ℕ) : coprime p i ∨ p ∣ i := by
+theorem coprime_or_dvd_of_prime {p} (pp : Prime p) (i : ℕ) : Coprime p i ∨ p ∣ i := by
   rw [pp.dvd_iff_not_coprime]; apply em
 #align nat.coprime_or_dvd_of_prime Nat.coprime_or_dvd_of_prime
 
-theorem coprime_of_lt_prime {n p} (n_pos : 0 < n) (hlt : n < p) (pp : Prime p) : coprime p n :=
+theorem coprime_of_lt_prime {n p} (n_pos : 0 < n) (hlt : n < p) (pp : Prime p) : Coprime p n :=
   (coprime_or_dvd_of_prime pp n).resolve_right fun h => lt_le_antisymm hlt (le_of_dvd n_pos h)
 #align nat.coprime_of_lt_prime Nat.coprime_of_lt_prime
 
 theorem eq_or_coprime_of_le_prime {n p} (n_pos : 0 < n) (hle : n ≤ p) (pp : Prime p) :
-    p = n ∨ coprime p n :=
+    p = n ∨ Coprime p n :=
   hle.eq_or_lt.imp Eq.symm fun h => coprime_of_lt_prime n_pos h pp
 #align nat.eq_or_coprime_of_le_prime Nat.eq_or_coprime_of_le_prime
 
@@ -696,7 +696,7 @@ theorem dvd_prime_pow {p : ℕ} (pp : Prime p) {m i : ℕ} : i ∣ p ^ m ↔ ∃
 
 theorem Prime.dvd_mul_of_dvd_ne {p1 p2 n : ℕ} (h_neq : p1 ≠ p2) (pp1 : Prime p1) (pp2 : Prime p2)
     (h1 : p1 ∣ n) (h2 : p2 ∣ n) : p1 * p2 ∣ n :=
-  coprime.mul_dvd_of_dvd_of_dvd ((coprime_primes pp1 pp2).mpr h_neq) h1 h2
+  Coprime.mul_dvd_of_dvd_of_dvd ((coprime_primes pp1 pp2).mpr h_neq) h1 h2
 #align nat.prime.dvd_mul_of_dvd_ne Nat.Prime.dvd_mul_of_dvd_ne
 
 /-- If `p` is prime,
diff --git a/Mathlib/Data/Nat/PrimeFin.lean b/Mathlib/Data/Nat/PrimeFin.lean
index ec28228795c2d..f1874bd20c685 100644
--- a/Mathlib/Data/Nat/PrimeFin.lean
+++ b/Mathlib/Data/Nat/PrimeFin.lean
@@ -55,7 +55,7 @@ theorem prime_pow_prime_divisor {p k : ℕ} (hk : k ≠ 0) (hp : Prime p) :
     (p ^ k).factors.toFinset = {p} := by simp [pow_factors_toFinset p hk, factors_prime hp]
 #align nat.prime_pow_prime_divisor Nat.prime_pow_prime_divisor
 
-theorem factors_mul_toFinset_of_coprime {a b : ℕ} (hab : coprime a b) :
+theorem factors_mul_toFinset_of_coprime {a b : ℕ} (hab : Coprime a b) :
     (a * b).factors.toFinset = a.factors.toFinset ∪ b.factors.toFinset :=
   (List.toFinset.ext <| mem_factors_mul_of_coprime hab).trans <| List.toFinset_union _ _
 #align nat.factors_mul_to_finset_of_coprime Nat.factors_mul_toFinset_of_coprime
diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean
index ba567e59f3d44..fb7b29f9d07b7 100644
--- a/Mathlib/Data/Nat/Squarefree.lean
+++ b/Mathlib/Data/Nat/Squarefree.lean
@@ -371,18 +371,18 @@ theorem sq_mul_squarefree (n : ℕ) : ∃ a b : ℕ, b ^ 2 * a = n ∧ Squarefre
 /-- `squarefree` is multiplicative. Note that the → direction does not require `hmn`
 and generalizes to arbitrary commutative monoids. See `squarefree.of_mul_left` and
 `squarefree.of_mul_right` above for auxiliary lemmas. -/
-theorem squarefree_mul {m n : ℕ} (hmn : m.coprime n) :
+theorem squarefree_mul {m n : ℕ} (hmn : m.Coprime n) :
     Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n := by
   simp only [squarefree_iff_prime_squarefree, ← sq, ← forall_and]
   refine' ball_congr fun p hp => _
   simp only [hmn.isPrimePow_dvd_mul (hp.isPrimePow.pow two_ne_zero), not_or]
 #align nat.squarefree_mul Nat.squarefree_mul
 
-theorem coprime_of_squarefree_mul {m n : ℕ} (h : Squarefree (m * n)) : m.coprime n :=
+theorem coprime_of_squarefree_mul {m n : ℕ} (h : Squarefree (m * n)) : m.Coprime n :=
   coprime_of_dvd fun p hp hm hn => squarefree_iff_prime_squarefree.mp h p hp (mul_dvd_mul hm hn)
 
 theorem squarefree_mul_iff {m n : ℕ} :
-    Squarefree (m * n) ↔ m.coprime n ∧ Squarefree m ∧ Squarefree n :=
+    Squarefree (m * n) ↔ m.Coprime n ∧ Squarefree m ∧ Squarefree n :=
   ⟨fun h => ⟨coprime_of_squarefree_mul h, (squarefree_mul $ coprime_of_squarefree_mul h).mp h⟩,
     fun h => (squarefree_mul h.1).mpr h.2⟩
 
diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean
index c94929f190366..5ccac5e1c233d 100644
--- a/Mathlib/Data/Nat/Totient.lean
+++ b/Mathlib/Data/Nat/Totient.lean
@@ -30,7 +30,7 @@ namespace Nat
 /-- Euler's totient function. This counts the number of naturals strictly less than `n` which are
 coprime with `n`. -/
 def totient (n : ℕ) : ℕ :=
-  ((range n).filter n.coprime).card
+  ((range n).filter n.Coprime).card
 #align nat.totient Nat.totient
 
 @[inherit_doc]
@@ -45,13 +45,13 @@ theorem totient_zero : φ 0 = 0 :=
 theorem totient_one : φ 1 = 1 := by simp [totient]
 #align nat.totient_one Nat.totient_one
 
-theorem totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter n.coprime).card :=
+theorem totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter n.Coprime).card :=
   rfl
 #align nat.totient_eq_card_coprime Nat.totient_eq_card_coprime
 
 /-- A characterisation of `Nat.totient` that avoids `Finset`. -/
-theorem totient_eq_card_lt_and_coprime (n : ℕ) : φ n = Nat.card { m | m < n ∧ n.coprime m } := by
-  let e : { m | m < n ∧ n.coprime m } ≃ Finset.filter n.coprime (Finset.range n) :=
+theorem totient_eq_card_lt_and_coprime (n : ℕ) : φ n = Nat.card { m | m < n ∧ n.Coprime m } := by
+  let e : { m | m < n ∧ n.Coprime m } ≃ Finset.filter n.Coprime (Finset.range n) :=
     { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
       invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
       left_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta]
@@ -74,13 +74,13 @@ theorem totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
 #align nat.totient_pos Nat.totient_pos
 
 theorem filter_coprime_Ico_eq_totient (a n : ℕ) :
-    ((Ico n (n + a)).filter (coprime a)).card = totient a := by
+    ((Ico n (n + a)).filter (Coprime a)).card = totient a := by
   rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
   exact periodic_coprime a
 #align nat.filter_coprime_Ico_eq_totient Nat.filter_coprime_Ico_eq_totient
 
 theorem Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
-    ((Ico k (k + n)).filter (coprime a)).card ≤ totient a * (n / a + 1) := by
+    ((Ico k (k + n)).filter (Coprime a)).card ≤ totient a * (n / a + 1) := by
   conv_lhs => rw [← Nat.mod_add_div n a]
   induction' n / a with i ih
   · rw [← filter_coprime_Ico_eq_totient a k]
@@ -88,20 +88,20 @@ theorem Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
       Nat.zero_eq, zero_add]
     --Porting note: below line was `mono`
     refine Finset.card_mono ?_
-    refine' monotone_filter_left a.coprime _
+    refine' monotone_filter_left a.Coprime _
     simp only [Finset.le_eq_subset]
     exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k)
   simp only [mul_succ]
   simp_rw [← add_assoc] at ih ⊢
   calc
-    (filter a.coprime (Ico k (k + n % a + a * i + a))).card = (filter a.coprime
+    (filter a.Coprime (Ico k (k + n % a + a * i + a))).card = (filter a.Coprime
         (Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card := by
       congr
       rw [Ico_union_Ico_eq_Ico]
       rw [add_assoc]
       exact le_self_add
       exact le_self_add
-    _ ≤ (filter a.coprime (Ico k (k + n % a + a * i))).card + a.totient := by
+    _ ≤ (filter a.Coprime (Ico k (k + n % a + a * i))).card + a.totient := by
       rw [filter_union, ← filter_coprime_Ico_eq_totient a (k + n % a + a * i)]
       apply card_union_le
     _ ≤ a.totient * i + a.totient + a.totient := add_le_add_right ih (totient a)
@@ -115,7 +115,7 @@ diamonds. -/
 theorem _root_.ZMod.card_units_eq_totient (n : ℕ) [NeZero n] [Fintype (ZMod n)ˣ] :
     Fintype.card (ZMod n)ˣ = φ n :=
   calc
-    Fintype.card (ZMod n)ˣ = Fintype.card { x : ZMod n // x.val.coprime n } :=
+    Fintype.card (ZMod n)ˣ = Fintype.card { x : ZMod n // x.val.Coprime n } :=
       Fintype.card_congr ZMod.unitsEquivCoprime
     _ = φ n := by
       obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
@@ -133,7 +133,7 @@ theorem totient_even {n : ℕ} (hn : 2 < n) : Even n.totient := by
   rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']
 #align nat.totient_even Nat.totient_even
 
-theorem totient_mul {m n : ℕ} (h : m.coprime n) : φ (m * n) = φ m * φ n :=
+theorem totient_mul {m n : ℕ} (h : m.Coprime n) : φ (m * n) = φ m * φ n :=
   if hmn0 : m * n = 0 then by
     cases' Nat.mul_eq_zero.1 hmn0 with h h <;>
       simp only [totient_zero, mul_zero, zero_mul, h]
@@ -153,7 +153,7 @@ theorem totient_div_of_dvd {n d : ℕ} (hnd : d ∣ n) :
   rcases hnd with ⟨x, rfl⟩
   rw [Nat.mul_div_cancel_left x hd0]
   apply Finset.card_congr fun k _ => d * k
-  · simp only [mem_filter, mem_range, and_imp, coprime]
+  · simp only [mem_filter, mem_range, and_imp, Coprime]
     refine' fun a ha1 ha2 => ⟨(mul_lt_mul_left hd0).2 ha1, _⟩
     rw [gcd_mul_left, ha2, mul_one]
   · simp [hd0.ne']
@@ -188,7 +188,7 @@ theorem sum_totient' (n : ℕ) : (∑ m in (range n.succ).filter (· ∣ n), φ
 /-- When `p` is prime, then the totient of `p ^ (n + 1)` is `p ^ n * (p - 1)` -/
 theorem totient_prime_pow_succ {p : ℕ} (hp : p.Prime) (n : ℕ) : φ (p ^ (n + 1)) = p ^ n * (p - 1) :=
   calc
-    φ (p ^ (n + 1)) = ((range (p ^ (n + 1))).filter (coprime (p ^ (n + 1)))).card :=
+    φ (p ^ (n + 1)) = ((range (p ^ (n + 1))).filter (Coprime (p ^ (n + 1)))).card :=
       totient_eq_card_coprime _
     _ = (range (p ^ (n + 1)) \ (range (p ^ n)).image (· * p)).card :=
       (congr_arg card
diff --git a/Mathlib/Data/PNat/Prime.lean b/Mathlib/Data/PNat/Prime.lean
index ad9cc5364822d..17ef5e3afe5dd 100644
--- a/Mathlib/Data/PNat/Prime.lean
+++ b/Mathlib/Data/PNat/Prime.lean
@@ -165,8 +165,8 @@ def Coprime (m n : ℕ+) : Prop :=
 #align pnat.coprime PNat.Coprime
 
 @[simp, norm_cast]
-theorem coprime_coe {m n : ℕ+} : Nat.coprime ↑m ↑n ↔ m.Coprime n := by
-  unfold coprime Coprime
+theorem coprime_coe {m n : ℕ+} : Nat.Coprime ↑m ↑n ↔ m.Coprime n := by
+  unfold Nat.Coprime Coprime
   rw [← coe_inj]
   simp
 #align pnat.coprime_coe PNat.coprime_coe
@@ -174,13 +174,13 @@ theorem coprime_coe {m n : ℕ+} : Nat.coprime ↑m ↑n ↔ m.Coprime n := by
 theorem Coprime.mul {k m n : ℕ+} : m.Coprime k → n.Coprime k → (m * n).Coprime k := by
   repeat' rw [← coprime_coe]
   rw [mul_coe]
-  apply Nat.coprime.mul
+  apply Nat.Coprime.mul
 #align pnat.coprime.mul PNat.Coprime.mul
 
 theorem Coprime.mul_right {k m n : ℕ+} : k.Coprime m → k.Coprime n → k.Coprime (m * n) := by
   repeat' rw [← coprime_coe]
   rw [mul_coe]
-  apply Nat.coprime.mul_right
+  apply Nat.Coprime.mul_right
 #align pnat.coprime.mul_right PNat.Coprime.mul_right
 
 theorem gcd_comm {m n : ℕ+} : m.gcd n = n.gcd m := by
@@ -204,7 +204,7 @@ theorem gcd_eq_right_iff_dvd {m n : ℕ+} : m ∣ n ↔ n.gcd m = m := by
 theorem Coprime.gcd_mul_left_cancel (m : ℕ+) {n k : ℕ+} :
     k.Coprime n → (k * m).gcd n = m.gcd n := by
   intro h; apply eq; simp only [gcd_coe, mul_coe]
-  apply Nat.coprime.gcd_mul_left_cancel; simpa
+  apply Nat.Coprime.gcd_mul_left_cancel; simpa
 #align pnat.coprime.gcd_mul_left_cancel PNat.Coprime.gcd_mul_left_cancel
 
 theorem Coprime.gcd_mul_right_cancel (m : ℕ+) {n k : ℕ+} : k.Coprime n → (m * k).gcd n = m.gcd n :=
@@ -255,7 +255,7 @@ theorem coprime_one {n : ℕ+} : n.Coprime 1 :=
 theorem Coprime.coprime_dvd_left {m k n : ℕ+} : m ∣ k → k.Coprime n → m.Coprime n := by
   rw [dvd_iff]
   repeat' rw [← coprime_coe]
-  apply Nat.coprime.coprime_dvd_left
+  apply Nat.Coprime.coprime_dvd_left
 #align pnat.coprime.coprime_dvd_left PNat.Coprime.coprime_dvd_left
 
 theorem Coprime.factor_eq_gcd_left {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m) (bn : b ∣ n) :
@@ -284,7 +284,7 @@ theorem Coprime.factor_eq_gcd_right_right {a b m n : ℕ+} (cop : m.Coprime n) (
 theorem Coprime.gcd_mul (k : ℕ+) {m n : ℕ+} (h : m.Coprime n) :
     k.gcd (m * n) = k.gcd m * k.gcd n := by
   rw [← coprime_coe] at h; apply eq
-  simp only [gcd_coe, mul_coe]; apply Nat.coprime.gcd_mul k h
+  simp only [gcd_coe, mul_coe]; apply Nat.Coprime.gcd_mul k h
 #align pnat.coprime.gcd_mul PNat.Coprime.gcd_mul
 
 theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m := by
@@ -295,8 +295,8 @@ theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m := by
   apply Nat.gcd_eq_left h
 #align pnat.gcd_eq_left PNat.gcd_eq_left
 
-theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k).coprime (n ^ l) := by
-  rw [← coprime_coe] at *; apply Nat.coprime.pow; apply h
+theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k).Coprime (n ^ l) := by
+  rw [← coprime_coe] at *; apply Nat.Coprime.pow; apply h
 #align pnat.coprime.pow PNat.Coprime.pow
 
 end Coprime
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
index 91cab7add1153..61fa0800e2f4f 100644
--- a/Mathlib/Data/Rat/Defs.lean
+++ b/Mathlib/Data/Rat/Defs.lean
@@ -118,7 +118,7 @@ theorem coe_int_eq_divInt (z : ℤ) : (z : ℚ) = z /. 1 := num_den'
 numbers of the form `n /. d` with `0 < d` and coprime `n`, `d`. -/
 @[elab_as_elim]
 def numDenCasesOn.{u} {C : ℚ → Sort u} :
-    ∀ (a : ℚ) (_ : ∀ n d, 0 < d → (Int.natAbs n).coprime d → C (n /. d)), C a
+    ∀ (a : ℚ) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a
   | ⟨n, d, h, c⟩, H => by rw [num_den']; exact H n d (Nat.pos_of_ne_zero h) c
 #align rat.num_denom_cases_on Rat.numDenCasesOn
 
diff --git a/Mathlib/Data/Rat/Denumerable.lean b/Mathlib/Data/Rat/Denumerable.lean
index bcc3c9f0b33c5..854b626f4692a 100644
--- a/Mathlib/Data/Rat/Denumerable.lean
+++ b/Mathlib/Data/Rat/Denumerable.lean
@@ -22,7 +22,7 @@ open Denumerable
 instance : Infinite ℚ :=
   Infinite.of_injective ((↑) : ℕ → ℚ) Nat.cast_injective
 
-private def denumerable_aux : ℚ ≃ { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.coprime x.2 }
+private def denumerable_aux : ℚ ≃ { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.Coprime x.2 }
     where
   toFun x := ⟨⟨x.1, x.2⟩, Nat.pos_of_ne_zero x.3, x.4⟩
   invFun x := ⟨x.1.1, x.1.2, ne_zero_of_lt x.2.1, x.2.2⟩
@@ -31,7 +31,7 @@ private def denumerable_aux : ℚ ≃ { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs
 
 /-- **Denumerability of the Rational Numbers** -/
 instance : Denumerable ℚ := by
-  let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.coprime x.2 }
+  let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.natAbs.Coprime x.2 }
   letI : Infinite T := Infinite.of_injective _ denumerable_aux.injective
   letI : Encodable T := Subtype.encodable
   letI : Denumerable T := ofEncodableOfInfinite T
diff --git a/Mathlib/Data/Rat/Encodable.lean b/Mathlib/Data/Rat/Encodable.lean
index 2c280b75f92af..49b25a93ff69c 100644
--- a/Mathlib/Data/Rat/Encodable.lean
+++ b/Mathlib/Data/Rat/Encodable.lean
@@ -20,7 +20,7 @@ This is kept separate from `Data.Rat.Defs` in order to minimize imports.
 namespace Rat
 
 instance : Encodable ℚ :=
-  Encodable.ofEquiv (Σn : ℤ, { d : ℕ // 0 < d ∧ n.natAbs.coprime d })
+  Encodable.ofEquiv (Σn : ℤ, { d : ℕ // 0 < d ∧ n.natAbs.Coprime d })
     ⟨fun ⟨a, b, c, d⟩ => ⟨a, b, Nat.pos_of_ne_zero c, d⟩,
       fun ⟨a, b, c, d⟩ => ⟨a, b, Nat.pos_iff_ne_zero.mp c, d⟩,
       fun _ => rfl, fun ⟨_, _, _, _⟩ => rfl⟩
diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean
index 72b9905fc1060..d06075f9a14a4 100644
--- a/Mathlib/Data/Rat/Floor.lean
+++ b/Mathlib/Data/Rat/Floor.lean
@@ -96,12 +96,12 @@ theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} : n % d = n - d
   rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_int_div_nat_eq_div]
 #align int.mod_nat_eq_sub_mul_floor_rat_div Int.mod_nat_eq_sub_mul_floor_rat_div
 
-theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.coprime d) :
-    ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.coprime d := by
+theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.Coprime d) :
+    ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d := by
   have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
   rw [← this]
-  have : d.coprime n := n_coprime_d.symm
-  rwa [Nat.coprime, Nat.gcd_rec] at this
+  have : d.Coprime n := n_coprime_d.symm
+  rwa [Nat.Coprime, Nat.gcd_rec] at this
 #align nat.coprime_sub_mul_floor_rat_div_of_coprime Nat.coprime_sub_mul_floor_rat_div_of_coprime
 
 namespace Rat
@@ -141,7 +141,7 @@ theorem fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) : (fract q⁻¹).n
   suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
     -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
     have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
-      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
+      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs by
         exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
       have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
       simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
@@ -154,7 +154,7 @@ theorem fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) : (fract q⁻¹).n
   -- use that `q.num` and `q.den` are coprime to show that q_inv is the unreduced reciprocal
   -- of `q`
   have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs := by
-    have coprime_q_denom_q_num : q.den.coprime q.num.natAbs := q.reduced.symm
+    have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm
     have : Int.natAbs q.den = q.den := by simp
     rw [← this] at coprime_q_denom_q_num
     rw [q_inv_def]
diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean
index 400709ab9248e..56cc618522406 100644
--- a/Mathlib/Data/Rat/Lemmas.lean
+++ b/Mathlib/Data/Rat/Lemmas.lean
@@ -97,12 +97,12 @@ theorem mul_den (q₁ q₂ : ℚ) :
 #align rat.mul_denom Rat.mul_den
 
 theorem mul_self_num (q : ℚ) : (q * q).num = q.num * q.num := by
-  rw [mul_num, Int.natAbs_mul, Nat.coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
+  rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
   exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)
 #align rat.mul_self_num Rat.mul_self_num
 
 theorem mul_self_den (q : ℚ) : (q * q).den = q.den * q.den := by
-  rw [Rat.mul_den, Int.natAbs_mul, Nat.coprime.gcd_eq_one, Nat.div_one]
+  rw [Rat.mul_den, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Nat.div_one]
   exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)
 #align rat.mul_self_denom Rat.mul_self_den
 
@@ -207,22 +207,22 @@ theorem den_div_cast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) : ((m : ℚ) / n).den
     rw [Int.cast_mul, mul_comm, mul_div_cancel _ hn, Rat.coe_int_den]
 #align rat.denom_div_cast_eq_one_iff Rat.den_div_cast_eq_one_iff
 
-theorem num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.coprime a.natAbs b.natAbs) :
+theorem num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
     (a / b : ℚ).num = a := by
   -- Porting note: was `lift b to ℕ using le_of_lt hb0`
   rw [←Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div,
     ←mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]
 #align rat.num_div_eq_of_coprime Rat.num_div_eq_of_coprime
 
-theorem den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.coprime a.natAbs b.natAbs) :
+theorem den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
     ((a / b : ℚ).den : ℤ) = b := by
   -- Porting note: was `lift b to ℕ using le_of_lt hb0`
   rw [←Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div,
     ←mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]
 #align rat.denom_div_eq_of_coprime Rat.den_div_eq_of_coprime
 
-theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.coprime a.natAbs b.natAbs)
-    (h2 : Nat.coprime c.natAbs d.natAbs) (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d := by
+theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime a.natAbs b.natAbs)
+    (h2 : Nat.Coprime c.natAbs d.natAbs) (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d := by
   apply And.intro
   · rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]
   · rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 0751a530e4a27..ebc4074264bc9 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -673,25 +673,25 @@ theorem eq_iff_modEq_nat (n : ℕ) {a b : ℕ} : (a : ZMod n) = b ↔ a ≡ b [M
     exact Iff.rfl
 #align zmod.eq_iff_modeq_nat ZMod.eq_iff_modEq_nat
 
-theorem coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : Nat.coprime x n) :
+theorem coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) :
     ((x : ZMod n) * (x : ZMod n)⁻¹) = 1 := by
-  rw [Nat.coprime, Nat.gcd_comm, Nat.gcd_rec] at h
+  rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h
   rw [mul_inv_eq_gcd, val_nat_cast, h, Nat.cast_one]
 #align zmod.coe_mul_inv_eq_one ZMod.coe_mul_inv_eq_one
 
 /-- `unitOfCoprime` makes an element of `(ZMod n)ˣ` given
   a natural number `x` and a proof that `x` is coprime to `n`  -/
-def unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.coprime x n) : (ZMod n)ˣ :=
+def unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) : (ZMod n)ˣ :=
   ⟨x, x⁻¹, coe_mul_inv_eq_one x h, by rw [mul_comm, coe_mul_inv_eq_one x h]⟩
 #align zmod.unit_of_coprime ZMod.unitOfCoprime
 
 @[simp]
-theorem coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.coprime x n) :
+theorem coe_unitOfCoprime {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) :
     (unitOfCoprime x h : ZMod n) = x :=
   rfl
 #align zmod.coe_unit_of_coprime ZMod.coe_unitOfCoprime
 
-theorem val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : Nat.coprime (u : ZMod n).val n := by
+theorem val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : Nat.Coprime (u : ZMod n).val n := by
   cases' n with n
   · rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp
   apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
@@ -726,7 +726,7 @@ theorem inv_mul_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a⁻¹ * a = 1 :
 -- TODO: this equivalence is true for `ZMod 0 = ℤ`, but needs to use different functions.
 /-- Equivalence between the units of `ZMod n` and
 the subtype of terms `x : ZMod n` for which `x.val` is coprime to `n` -/
-def unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // Nat.coprime x.val n }
+def unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // Nat.Coprime x.val n }
     where
   toFun x := ⟨x, val_coe_unit_coprime x⟩
   invFun x := unitOfCoprime x.1.val x.2
@@ -740,7 +740,7 @@ def unitsEquivCoprime {n : ℕ} [NeZero n] : (ZMod n)ˣ ≃ { x : ZMod n // Nat.
 See `Ideal.quotientInfRingEquivPiQuotient` for the Chinese remainder theorem for ideals in any
 ring.
 -/
-def chineseRemainder {m n : ℕ} (h : m.coprime n) : ZMod (m * n) ≃+* ZMod m × ZMod n :=
+def chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m × ZMod n :=
   let to_fun : ZMod (m * n) → ZMod m × ZMod n :=
     ZMod.castHom (show m.lcm n ∣ m * n by simp [Nat.lcm_dvd_iff]) (ZMod m × ZMod n)
   let inv_fun : ZMod m × ZMod n → ZMod (m * n) := fun x =>
@@ -1095,7 +1095,7 @@ variable (p : ℕ) [Fact p.Prime]
 private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 := by
   obtain ⟨k, rfl⟩ := nat_cast_zmod_surjective a
   apply coe_mul_inv_eq_one
-  apply Nat.coprime.symm
+  apply Nat.Coprime.symm
   rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
 
 /-- Field structure on `ZMod p` if `p` is prime. -/
diff --git a/Mathlib/Dynamics/PeriodicPts.lean b/Mathlib/Dynamics/PeriodicPts.lean
index bf37266922568..5eca0bfc953c7 100644
--- a/Mathlib/Dynamics/PeriodicPts.lean
+++ b/Mathlib/Dynamics/PeriodicPts.lean
@@ -435,13 +435,13 @@ theorem Commute.minimalPeriod_of_comp_dvd_mul {g : α → α} (h : Commute f g)
 #align function.commute.minimal_period_of_comp_dvd_mul Function.Commute.minimalPeriod_of_comp_dvd_mul
 
 theorem Commute.minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Commute f g)
-    (hco : coprime (minimalPeriod f x) (minimalPeriod g x)) :
+    (hco : Coprime (minimalPeriod f x) (minimalPeriod g x)) :
     minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x := by
   apply h.minimalPeriod_of_comp_dvd_mul.antisymm
   suffices
     ∀ {f g : α → α},
       Commute f g →
-        coprime (minimalPeriod f x) (minimalPeriod g x) →
+        Coprime (minimalPeriod f x) (minimalPeriod g x) →
           minimalPeriod f x ∣ minimalPeriod (f ∘ g) x from
     hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
   intro f g h hco
@@ -457,7 +457,7 @@ private theorem minimalPeriod_iterate_eq_div_gcd_aux (h : 0 < gcd (minimalPeriod
     rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _),
       mul_comm, Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul]
     exact (isPeriodicPt_minimalPeriod f x).iterate _
-  · apply coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
+  · apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
     apply Nat.dvd_of_mul_dvd_mul_right h
     rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
       mul_comm]
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
index 05e9b05e825cf..a5b2570c5ad1f 100644
--- a/Mathlib/FieldTheory/Finite/Basic.lean
+++ b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -370,7 +370,7 @@ theorem ZMod.pow_totient {n : ℕ} (x : (ZMod n)ˣ) : x ^ φ n = 1 := by
 
 /-- The **Fermat-Euler totient theorem**. `ZMod.pow_totient` is an alternative statement
   of the same theorem. -/
-theorem Nat.ModEq.pow_totient {x n : ℕ} (h : Nat.coprime x n) : x ^ φ n ≡ 1 [MOD n] := by
+theorem Nat.ModEq.pow_totient {x n : ℕ} (h : Nat.Coprime x n) : x ^ φ n ≡ 1 [MOD n] := by
   rw [← ZMod.eq_iff_modEq_nat]
   let x' : Units (ZMod n) := ZMod.unitOfCoprime _ h
   have := ZMod.pow_totient x'
diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean
index de1fa1d67c19c..c0950949ca21d 100644
--- a/Mathlib/GroupTheory/Complement.lean
+++ b/Mathlib/GroupTheory/Complement.lean
@@ -681,7 +681,7 @@ theorem isComplement'_iff_card_mul_and_disjoint [Fintype G] [Fintype H] [Fintype
 
 theorem isComplement'_of_coprime [Fintype G] [Fintype H] [Fintype K]
     (h1 : Fintype.card H * Fintype.card K = Fintype.card G)
-    (h2 : Nat.coprime (Fintype.card H) (Fintype.card K)) : IsComplement' H K :=
+    (h2 : Nat.Coprime (Fintype.card H) (Fintype.card K)) : IsComplement' H K :=
   isComplement'_of_card_mul_and_disjoint h1 (disjoint_iff.mpr (inf_eq_bot_of_coprime h2))
 #align subgroup.is_complement'_of_coprime Subgroup.isComplement'_of_coprime
 
diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean
index 101b7ec34cb57..a5bd4a7e4dfb2 100644
--- a/Mathlib/GroupTheory/Exponent.lean
+++ b/Mathlib/GroupTheory/Exponent.lean
@@ -306,7 +306,7 @@ theorem exponent_eq_iSup_orderOf (h : ∀ g : G, 0 < orderOf g) :
   have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
     rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
   obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
-  have hcoprime : (orderOf (t ^ p ^ k)).coprime (orderOf g) := by
+  have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g) := by
     rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
     apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
     nth_rw 1 [← pow_one p]
@@ -386,4 +386,3 @@ theorem card_dvd_exponent_pow_rank' {n : ℕ} (hG : ∀ g : G, g ^ n = 1) :
 #align card_dvd_exponent_nsmul_rank' card_dvd_exponent_nsmul_rank'
 
 end CommGroup
-
diff --git a/Mathlib/GroupTheory/NoncommPiCoprod.lean b/Mathlib/GroupTheory/NoncommPiCoprod.lean
index bec1f196e3583..f26f4eb7a1cab 100644
--- a/Mathlib/GroupTheory/NoncommPiCoprod.lean
+++ b/Mathlib/GroupTheory/NoncommPiCoprod.lean
@@ -233,7 +233,7 @@ variable (hcomm)
 
 @[to_additive]
 theorem independent_range_of_coprime_order [Finite ι] [∀ i, Fintype (H i)]
-    (hcoprime : ∀ i j, i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))) :
+    (hcoprime : ∀ i j, i ≠ j → Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
     CompleteLattice.Independent fun i => (ϕ i).range := by
   cases nonempty_fintype ι
   classical
@@ -333,7 +333,7 @@ variable (hcomm)
 
 @[to_additive]
 theorem independent_of_coprime_order [Finite ι] [∀ i, Fintype (H i)]
-    (hcoprime : ∀ i j, i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))) :
+    (hcoprime : ∀ i j, i ≠ j → Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
     CompleteLattice.Independent H := by
   simpa using
     MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index 09da3cec64798..5b7439a58c916 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -293,7 +293,7 @@ theorem orderOf_map_dvd {H : Type*} [Monoid H] (ψ : G →* H) (x : G) :
 #align add_order_of_map_dvd addOrderOf_map_dvd
 
 @[to_additive]
-theorem exists_pow_eq_self_of_coprime (h : n.coprime (orderOf x)) : ∃ m : ℕ, (x ^ n) ^ m = x := by
+theorem exists_pow_eq_self_of_coprime (h : n.Coprime (orderOf x)) : ∃ m : ℕ, (x ^ n) ^ m = x := by
   by_cases h0 : orderOf x = 0
   · rw [h0, coprime_zero_right] at h
     exact ⟨1, by rw [h, pow_one, pow_one]⟩
@@ -374,7 +374,7 @@ theorem orderOf_pow'' (h : IsOfFinOrder x) : orderOf (x ^ n) = orderOf x / gcd (
 #align add_order_of_nsmul'' addOrderOf_nsmul''
 
 @[to_additive]
-theorem orderOf_pow_coprime (h : (orderOf y).coprime m) : orderOf (y ^ m) = orderOf y := by
+theorem orderOf_pow_coprime (h : (orderOf y).Coprime m) : orderOf (y ^ m) = orderOf y := by
   by_cases hg : orderOf y = 0
   · rw [m.coprime_zero_left.mp (hg ▸ h), pow_one]
   · rw [orderOf_pow'' y m (hg.imp_symm orderOf_eq_zero), h.gcd_eq_one, Nat.div_one]
@@ -413,7 +413,7 @@ theorem orderOf_mul_dvd_mul_orderOf : orderOf (x * y) ∣ orderOf x * orderOf y
 #align add_commute.add_order_of_add_dvd_mul_add_order_of AddCommute.addOrderOf_add_dvd_mul_addOrderOf
 
 @[to_additive addOrderOf_add_eq_mul_addOrderOf_of_coprime]
-theorem orderOf_mul_eq_mul_orderOf_of_coprime (hco : (orderOf x).coprime (orderOf y)) :
+theorem orderOf_mul_eq_mul_orderOf_of_coprime (hco : (orderOf x).Coprime (orderOf y)) :
     orderOf (x * y) = orderOf x * orderOf y := by
   rw [orderOf, ← comp_mul_left]
   exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco
@@ -993,7 +993,7 @@ theorem zpow_eq_mod_card (n : ℤ) : x ^ n = x ^ (n % Fintype.card G : ℤ) := b
 
 /-- If `gcd(|G|,n)=1` then the `n`th power map is a bijection -/
 @[to_additive (attr := simps) "If `gcd(|G|,n)=1` then the smul by `n` is a bijection"]
-noncomputable def powCoprime {G : Type*} [Group G] (h : (Nat.card G).coprime n) : G ≃ G
+noncomputable def powCoprime {G : Type*} [Group G] (h : (Nat.card G).Coprime n) : G ≃ G
     where
   toFun g := g ^ n
   invFun g := g ^ (Nat.card G).gcdB n
@@ -1011,13 +1011,13 @@ noncomputable def powCoprime {G : Type*} [Group G] (h : (Nat.card G).coprime n)
 #align nsmul_coprime nsmulCoprime
 
 @[to_additive] -- Porting note: simp can prove this (so removed simp)
-theorem powCoprime_one {G : Type*} [Group G] (h : (Nat.card G).coprime n) : powCoprime h 1 = 1 :=
+theorem powCoprime_one {G : Type*} [Group G] (h : (Nat.card G).Coprime n) : powCoprime h 1 = 1 :=
   one_pow n
 #align pow_coprime_one powCoprime_one
 #align nsmul_coprime_zero nsmulCoprime_zero
 
 @[to_additive] -- Porting note: simp can prove this (so removed simp)
-theorem powCoprime_inv {G : Type*} [Group G] (h : (Nat.card G).coprime n) {g : G} :
+theorem powCoprime_inv {G : Type*} [Group G] (h : (Nat.card G).Coprime n) {g : G} :
     powCoprime h g⁻¹ = (powCoprime h g)⁻¹ :=
   inv_pow g n
 #align pow_coprime_inv powCoprime_inv
@@ -1025,7 +1025,7 @@ theorem powCoprime_inv {G : Type*} [Group G] (h : (Nat.card G).coprime n) {g : G
 
 @[to_additive add_inf_eq_bot_of_coprime]
 theorem inf_eq_bot_of_coprime {G : Type*} [Group G] {H K : Subgroup G} [Fintype H] [Fintype K]
-    (h : Nat.coprime (Fintype.card H) (Fintype.card K)) : H ⊓ K = ⊥ := by
+    (h : Nat.Coprime (Fintype.card H) (Fintype.card K)) : H ⊓ K = ⊥ := by
   refine' (H ⊓ K).eq_bot_iff_forall.mpr fun x hx => _
   rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← h.gcd_eq_one, Nat.dvd_gcd_iff]
   exact
diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean
index a94d534642d53..acd152bd3e522 100644
--- a/Mathlib/GroupTheory/PGroup.lean
+++ b/Mathlib/GroupTheory/PGroup.lean
@@ -95,14 +95,14 @@ theorem of_equiv {H : Type*} [Group H] (ϕ : G ≃* H) : IsPGroup p H :=
   hG.of_surjective ϕ.toMonoidHom ϕ.surjective
 #align is_p_group.of_equiv IsPGroup.of_equiv
 
-theorem orderOf_coprime {n : ℕ} (hn : p.coprime n) (g : G) : (orderOf g).coprime n :=
+theorem orderOf_coprime {n : ℕ} (hn : p.Coprime n) (g : G) : (orderOf g).Coprime n :=
   let ⟨k, hk⟩ := hG g
   (hn.pow_left k).coprime_dvd_left (orderOf_dvd_of_pow_eq_one hk)
 #align is_p_group.order_of_coprime IsPGroup.orderOf_coprime
 
 /-- If `gcd(p,n) = 1`, then the `n`th power map is a bijection. -/
-noncomputable def powEquiv {n : ℕ} (hn : p.coprime n) : G ≃ G :=
-  let h : ∀ g : G, (Nat.card (Subgroup.zpowers g)).coprime n := fun g =>
+noncomputable def powEquiv {n : ℕ} (hn : p.Coprime n) : G ≃ G :=
+  let h : ∀ g : G, (Nat.card (Subgroup.zpowers g)).Coprime n := fun g =>
     order_eq_card_zpowers' g ▸ hG.orderOf_coprime hn g
   { toFun := (· ^ n)
     invFun := fun g => (powCoprime (h g)).symm ⟨g, Subgroup.mem_zpowers g⟩
@@ -115,12 +115,12 @@ noncomputable def powEquiv {n : ℕ} (hn : p.coprime n) : G ≃ G :=
 #align is_p_group.pow_equiv IsPGroup.powEquiv
 
 @[simp]
-theorem powEquiv_apply {n : ℕ} (hn : p.coprime n) (g : G) : hG.powEquiv hn g = g ^ n :=
+theorem powEquiv_apply {n : ℕ} (hn : p.Coprime n) (g : G) : hG.powEquiv hn g = g ^ n :=
   rfl
 #align is_p_group.pow_equiv_apply IsPGroup.powEquiv_apply
 
 @[simp]
-theorem powEquiv_symm_apply {n : ℕ} (hn : p.coprime n) (g : G) :
+theorem powEquiv_symm_apply {n : ℕ} (hn : p.Coprime n) (g : G) :
     (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n := by rw [order_eq_card_zpowers']; rfl
 #align is_p_group.pow_equiv_symm_apply IsPGroup.powEquiv_symm_apply
 
@@ -341,7 +341,7 @@ theorem to_sup_of_normal_left' {H K : Subgroup G} (hH : IsPGroup p H) (hK : IsPG
 theorem coprime_card_of_ne {G₂ : Type*} [Group G₂] (p₁ p₂ : ℕ) [hp₁ : Fact p₁.Prime]
     [hp₂ : Fact p₂.Prime] (hne : p₁ ≠ p₂) (H₁ : Subgroup G) (H₂ : Subgroup G₂) [Fintype H₁]
     [Fintype H₂] (hH₁ : IsPGroup p₁ H₁) (hH₂ : IsPGroup p₂ H₂) :
-    Nat.coprime (Fintype.card H₁) (Fintype.card H₂) := by
+    Nat.Coprime (Fintype.card H₁) (Fintype.card H₂) := by
   obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁; rw [heq₁]; clear heq₁
   obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂; rw [heq₂]; clear heq₂
   exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne
@@ -409,4 +409,3 @@ theorem commutative_of_card_eq_prime_sq (hG : card G = p ^ 2) : ∀ a b : G, a *
 end P2comm
 
 end IsPGroup
-
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
index 2605e1918b96e..272dec968e036 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -639,7 +639,7 @@ theorem IsCycle.support_pow_of_pos_of_lt_orderOf (hf : IsCycle f) {n : ℕ} (npo
 #align equiv.perm.is_cycle.support_pow_of_pos_of_lt_order_of Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf
 
 theorem IsCycle.pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
-    IsCycle (f ^ n) ↔ n.coprime (orderOf f) := by
+    IsCycle (f ^ n) ↔ n.Coprime (orderOf f) := by
   classical
     cases nonempty_fintype β
     constructor
@@ -723,8 +723,8 @@ theorem IsCycle.isCycle_pow_pos_of_lt_prime_order [Finite β] {f : Perm β} (hf
     (hf' : (orderOf f).Prime) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) : IsCycle (f ^ n) := by
   classical
     cases nonempty_fintype β
-    have : n.coprime (orderOf f) := by
-      refine' Nat.coprime.symm _
+    have : n.Coprime (orderOf f) := by
+      refine' Nat.Coprime.symm _
       rw [Nat.Prime.coprime_iff_not_dvd hf']
       exact Nat.not_dvd_of_pos_of_lt hn hn'
     obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime this
@@ -1660,7 +1660,7 @@ theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.su
   exact step4 y z
 #align equiv.perm.closure_cycle_adjacent_swap Equiv.Perm.closure_cycle_adjacent_swap
 
-theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.coprime n (Fintype.card α))
+theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.Coprime n (Fintype.card α))
     (h1 : IsCycle σ) (h2 : σ.support = Finset.univ) (x : α) :
     closure ({σ, swap x ((σ ^ n) x)} : Set (Perm α)) = ⊤ := by
   rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
@@ -1683,7 +1683,7 @@ theorem closure_prime_cycle_swap {σ τ : Perm α} (h0 : (Fintype.card α).Prime
       (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
   rw [h5, ← hi]
   refine'
-    closure_cycle_coprime_swap (Nat.coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 _)) h1 h2 x
+    closure_cycle_coprime_swap (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 _)) h1 h2 x
   cases' h with m hm
   rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
     one_apply] at hi
diff --git a/Mathlib/GroupTheory/Perm/Sign.lean b/Mathlib/GroupTheory/Perm/Sign.lean
index 05ae132b86102..bd849bee13872 100644
--- a/Mathlib/GroupTheory/Perm/Sign.lean
+++ b/Mathlib/GroupTheory/Perm/Sign.lean
@@ -194,7 +194,7 @@ section Fintype
 
 variable [Fintype α]
 
-theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.coprime n (orderOf σ)) :
+theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) :
     (σ ^ n).support = σ.support := by
   obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
   exact
diff --git a/Mathlib/GroupTheory/SchurZassenhaus.lean b/Mathlib/GroupTheory/SchurZassenhaus.lean
index cb373081dc6bc..cfa895ef30e87 100644
--- a/Mathlib/GroupTheory/SchurZassenhaus.lean
+++ b/Mathlib/GroupTheory/SchurZassenhaus.lean
@@ -96,7 +96,7 @@ theorem smul_diff' (h : H) :
   exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)
 #align subgroup.smul_diff' Subgroup.smul_diff'
 
-theorem eq_one_of_smul_eq_one (hH : Nat.coprime (Nat.card H) H.index) (α : H.QuotientDiff)
+theorem eq_one_of_smul_eq_one (hH : Nat.Coprime (Nat.card H) H.index) (α : H.QuotientDiff)
   (h : H) : h • α = α → h = 1 :=
   Quotient.inductionOn' α fun α hα =>
     (powCoprime hH).injective <|
@@ -107,7 +107,7 @@ theorem eq_one_of_smul_eq_one (hH : Nat.coprime (Nat.card H) H.index) (α : H.Qu
 
 #align subgroup.eq_one_of_smul_eq_one Subgroup.eq_one_of_smul_eq_one
 
-theorem exists_smul_eq (hH : Nat.coprime (Nat.card H) H.index) (α β : H.QuotientDiff) :
+theorem exists_smul_eq (hH : Nat.Coprime (Nat.card H) H.index) (α β : H.QuotientDiff) :
     ∃ h : H, h • α = β :=
   Quotient.inductionOn' α
     (Quotient.inductionOn' β fun β α =>
@@ -120,12 +120,12 @@ theorem exists_smul_eq (hH : Nat.coprime (Nat.card H) H.index) (α β : H.Quotie
 #align subgroup.exists_smul_eq Subgroup.exists_smul_eq
 
 theorem isComplement'_stabilizer_of_coprime {α : H.QuotientDiff}
-    (hH : Nat.coprime (Nat.card H) H.index) : IsComplement' H (stabilizer G α) :=
+    (hH : Nat.Coprime (Nat.card H) H.index) : IsComplement' H (stabilizer G α) :=
   isComplement'_stabilizer α (eq_one_of_smul_eq_one hH α) fun g => exists_smul_eq hH (g • α) α
 #align subgroup.is_complement'_stabilizer_of_coprime Subgroup.isComplement'_stabilizer_of_coprime
 
 /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
-private theorem exists_right_complement'_of_coprime_aux (hH : Nat.coprime (Nat.card H) H.index) :
+private theorem exists_right_complement'_of_coprime_aux (hH : Nat.Coprime (Nat.card H) H.index) :
     ∃ K : Subgroup G, IsComplement' H K :=
   instNonempty.elim fun α => ⟨stabilizer G α, isComplement'_stabilizer_of_coprime hH⟩
 
@@ -145,11 +145,11 @@ The proof is by contradiction. We assume that `G` is a minimal counterexample to
 
 
 variable {G : Type u} [Group G] [Fintype G] {N : Subgroup G} [Normal N]
-  (h1 : Nat.coprime (Fintype.card N) N.index)
+  (h1 : Nat.Coprime (Fintype.card N) N.index)
   (h2 :
     ∀ (G' : Type u) [Group G'] [Fintype G'],
       ∀ (_ : Fintype.card G' < Fintype.card G) {N' : Subgroup G'} [N'.Normal]
-        (_ : Nat.coprime (Fintype.card N') N'.index), ∃ H' : Subgroup G', IsComplement' N' H')
+        (_ : Nat.Coprime (Fintype.card N') N'.index), ∃ H' : Subgroup G', IsComplement' N' H')
   (h3 : ∀ H : Subgroup G, ¬IsComplement' N H)
 
 /-! We will arrive at a contradiction via the following steps:
@@ -178,7 +178,7 @@ private theorem step1 (K : Subgroup G) (hK : K ⊔ N = ⊤) : K = ⊤ := by
   have h5 : Fintype.card K < Fintype.card G := by
     rw [← K.index_mul_card]
     exact lt_mul_of_one_lt_left Fintype.card_pos (one_lt_index_of_ne_top h3)
-  have h6 : Nat.coprime (Fintype.card (N.comap K.subtype)) (N.comap K.subtype).index := by
+  have h6 : Nat.Coprime (Fintype.card (N.comap K.subtype)) (N.comap K.subtype).index := by
     rw [h4]
     exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
   obtain ⟨H, hH⟩ := h2 K h5 h6
@@ -188,7 +188,7 @@ private theorem step1 (K : Subgroup G) (hK : K ⊔ N = ⊤) : K = ⊤ := by
       subtype_range, ←relindex_sup_right, hK, relindex_top_right]
   have h7 : Fintype.card N * Fintype.card (H.map K.subtype) = Fintype.card G := by
     rw [hH, ← N.index_mul_card, mul_comm]
-  have h8 : (Fintype.card N).coprime (Fintype.card (H.map K.subtype)) := by
+  have h8 : (Fintype.card N).Coprime (Fintype.card (H.map K.subtype)) := by
     rwa [hH]
   exact ⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩
 
@@ -203,7 +203,7 @@ private theorem step2 (K : Subgroup G) [K.Normal] (hK : K ≤ N) : K = ⊥ ∨ K
       lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite)
         (K.one_lt_card_iff_ne_bot.mpr h4.1)
   have h6 :
-    (Fintype.card (N.map (QuotientGroup.mk' K))).coprime (N.map (QuotientGroup.mk' K)).index := by
+    (Fintype.card (N.map (QuotientGroup.mk' K))).Coprime (N.map (QuotientGroup.mk' K)).index := by
     have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
     have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
     rw [index_map]
@@ -267,7 +267,7 @@ variable {n : ℕ} {G : Type u} [Group G]
 
 /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
 private theorem exists_right_complement'_of_coprime_aux' [Fintype G] (hG : Fintype.card G = n)
-    {N : Subgroup G} [N.Normal] (hN : Nat.coprime (Fintype.card N) N.index) :
+    {N : Subgroup G} [N.Normal] (hN : Nat.Coprime (Fintype.card N) N.index) :
     ∃ H : Subgroup G, IsComplement' N H := by
   revert G
   apply Nat.strongInductionOn n
@@ -281,7 +281,7 @@ private theorem exists_right_complement'_of_coprime_aux' [Fintype G] (hG : Finty
   If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
   subgroup `K` which is a (right) complement of `H`. -/
 theorem exists_right_complement'_of_coprime_of_fintype [Fintype G] {N : Subgroup G} [N.Normal]
-    (hN : Nat.coprime (Fintype.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H :=
+    (hN : Nat.Coprime (Fintype.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H :=
   exists_right_complement'_of_coprime_aux' rfl hN
 #align subgroup.exists_right_complement'_of_coprime_of_fintype Subgroup.exists_right_complement'_of_coprime_of_fintype
 
@@ -289,7 +289,7 @@ theorem exists_right_complement'_of_coprime_of_fintype [Fintype G] {N : Subgroup
   If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
   subgroup `K` which is a (right) complement of `H`. -/
 theorem exists_right_complement'_of_coprime {N : Subgroup G} [N.Normal]
-    (hN : Nat.coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H := by
+    (hN : Nat.Coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H := by
   by_cases hN1 : Nat.card N = 0
   · rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN
     rw [hN]
@@ -312,7 +312,7 @@ theorem exists_right_complement'_of_coprime {N : Subgroup G} [N.Normal]
   If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
   subgroup `K` which is a (left) complement of `H`. -/
 theorem exists_left_complement'_of_coprime_of_fintype [Fintype G] {N : Subgroup G} [N.Normal]
-    (hN : Nat.coprime (Fintype.card N) N.index) : ∃ H : Subgroup G, IsComplement' H N :=
+    (hN : Nat.Coprime (Fintype.card N) N.index) : ∃ H : Subgroup G, IsComplement' H N :=
   Exists.imp (fun _ => IsComplement'.symm) (exists_right_complement'_of_coprime_of_fintype hN)
 #align subgroup.exists_left_complement'_of_coprime_of_fintype Subgroup.exists_left_complement'_of_coprime_of_fintype
 
@@ -320,7 +320,7 @@ theorem exists_left_complement'_of_coprime_of_fintype [Fintype G] {N : Subgroup
   If `H : Subgroup G` is normal, and has order coprime to its index, then there exists a
   subgroup `K` which is a (left) complement of `H`. -/
 theorem exists_left_complement'_of_coprime {N : Subgroup G} [N.Normal]
-    (hN : Nat.coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' H N :=
+    (hN : Nat.Coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' H N :=
   Exists.imp (fun _ => IsComplement'.symm) (exists_right_complement'_of_coprime hN)
 #align subgroup.exists_left_complement'_of_coprime Subgroup.exists_left_complement'_of_coprime
 
diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
index d9cc54b6af9d7..d89667509b347 100644
--- a/Mathlib/GroupTheory/Sylow.lean
+++ b/Mathlib/GroupTheory/Sylow.lean
@@ -672,7 +672,7 @@ theorem dvd_card_of_dvd_card [Fintype G] {p : ℕ} [Fact p.Prime] (P : Sylow p G
 
 /-- Sylow subgroups are Hall subgroups. -/
 theorem card_coprime_index [Fintype G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) :
-    (card P).coprime (index (P : Subgroup G)) :=
+    (card P).Coprime (index (P : Subgroup G)) :=
   let ⟨_n, hn⟩ := IsPGroup.iff_card.mp P.2
   hn.symm ▸ (hp.1.coprime_pow_of_not_dvd (not_dvd_index_sylow P index_ne_zero_of_finite)).symm
 #align sylow.card_coprime_index Sylow.card_coprime_index
diff --git a/Mathlib/Init/Data/Nat/GCD.lean b/Mathlib/Init/Data/Nat/GCD.lean
index f4e38e53a4b4d..76cafc5a2e8e2 100644
--- a/Mathlib/Init/Data/Nat/GCD.lean
+++ b/Mathlib/Init/Data/Nat/GCD.lean
@@ -35,7 +35,7 @@ theorem gcd_def (x y : ℕ) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases x <;> simp [Nat.gcd_succ]
 #align nat.gcd_def Nat.gcd_def
 
-#align nat.coprime Nat.coprime
+#align nat.coprime Nat.Coprime
 
 end Nat
 
@@ -88,44 +88,44 @@ end Nat
 #align nat.lcm_assoc Nat.lcm_assoc
 #align nat.lcm_ne_zero Nat.lcm_ne_zero
 #align nat.coprime_iff_gcd_eq_one Nat.coprime_iff_gcd_eq_one
-#align nat.coprime.gcd_eq_one Nat.coprime.gcd_eq_one
-#align nat.coprime.symm Nat.coprime.symm
+#align nat.coprime.gcd_eq_one Nat.Coprime.gcd_eq_one
+#align nat.coprime.symm Nat.Coprime.symm
 #align nat.coprime_comm Nat.coprime_comm
-#align nat.coprime.dvd_of_dvd_mul_right Nat.coprime.dvd_of_dvd_mul_right
-#align nat.coprime.dvd_of_dvd_mul_left Nat.coprime.dvd_of_dvd_mul_left
-#align nat.coprime.gcd_mul_left_cancel Nat.coprime.gcd_mul_left_cancel
-#align nat.coprime.gcd_mul_right_cancel Nat.coprime.gcd_mul_right_cancel
-#align nat.coprime.gcd_mul_left_cancel_right Nat.coprime.gcd_mul_left_cancel_right
-#align nat.coprime.gcd_mul_right_cancel_right Nat.coprime.gcd_mul_right_cancel_right
+#align nat.coprime.dvd_of_dvd_mul_right Nat.Coprime.dvd_of_dvd_mul_right
+#align nat.coprime.dvd_of_dvd_mul_left Nat.Coprime.dvd_of_dvd_mul_left
+#align nat.coprime.gcd_mul_left_cancel Nat.Coprime.gcd_mul_left_cancel
+#align nat.coprime.gcd_mul_right_cancel Nat.Coprime.gcd_mul_right_cancel
+#align nat.coprime.gcd_mul_left_cancel_right Nat.Coprime.gcd_mul_left_cancel_right
+#align nat.coprime.gcd_mul_right_cancel_right Nat.Coprime.gcd_mul_right_cancel_right
 #align nat.coprime_div_gcd_div_gcd Nat.coprime_div_gcd_div_gcd
 #align nat.not_coprime_of_dvd_of_dvd Nat.not_coprime_of_dvd_of_dvd
 #align nat.exists_coprime Nat.exists_coprime
 #align nat.exists_coprime' Nat.exists_coprime'
-#align nat.coprime.mul Nat.coprime.mul
-#align nat.coprime.mul_right Nat.coprime.mul_right
-#align nat.coprime.coprime_dvd_left Nat.coprime.coprime_dvd_left
-#align nat.coprime.coprime_dvd_right Nat.coprime.coprime_dvd_right
-#align nat.coprime.coprime_mul_left Nat.coprime.coprime_mul_left
-#align nat.coprime.coprime_mul_right Nat.coprime.coprime_mul_right
-#align nat.coprime.coprime_mul_left_right Nat.coprime.coprime_mul_left_right
-#align nat.coprime.coprime_mul_right_right Nat.coprime.coprime_mul_right_right
-#align nat.coprime.coprime_div_left Nat.coprime.coprime_div_left
-#align nat.coprime.coprime_div_right Nat.coprime.coprime_div_right
+#align nat.coprime.mul Nat.Coprime.mul
+#align nat.coprime.mul_right Nat.Coprime.mul_right
+#align nat.coprime.coprime_dvd_left Nat.Coprime.coprime_dvd_left
+#align nat.coprime.coprime_dvd_right Nat.Coprime.coprime_dvd_right
+#align nat.coprime.coprime_mul_left Nat.Coprime.coprime_mul_left
+#align nat.coprime.coprime_mul_right Nat.Coprime.coprime_mul_right
+#align nat.coprime.coprime_mul_left_right Nat.Coprime.coprime_mul_left_right
+#align nat.coprime.coprime_mul_right_right Nat.Coprime.coprime_mul_right_right
+#align nat.coprime.coprime_div_left Nat.Coprime.coprime_div_left
+#align nat.coprime.coprime_div_right Nat.Coprime.coprime_div_right
 #align nat.coprime_mul_iff_left Nat.coprime_mul_iff_left
 #align nat.coprime_mul_iff_right Nat.coprime_mul_iff_right
-#align nat.coprime.gcd_left Nat.coprime.gcd_left
-#align nat.coprime.gcd_right Nat.coprime.gcd_right
-#align nat.coprime.gcd_both Nat.coprime.gcd_both
-#align nat.coprime.mul_dvd_of_dvd_of_dvd Nat.coprime.mul_dvd_of_dvd_of_dvd
+#align nat.coprime.gcd_left Nat.Coprime.gcd_left
+#align nat.coprime.gcd_right Nat.Coprime.gcd_right
+#align nat.coprime.gcd_both Nat.Coprime.gcd_both
+#align nat.coprime.mul_dvd_of_dvd_of_dvd Nat.Coprime.mul_dvd_of_dvd_of_dvd
 #align nat.coprime_zero_left Nat.coprime_zero_left
 #align nat.coprime_zero_right Nat.coprime_zero_right
 #align nat.coprime_one_left Nat.coprime_one_left
 #align nat.coprime_one_right Nat.coprime_one_right
 #align nat.coprime_self Nat.coprime_self
-#align nat.coprime.pow_left Nat.coprime.pow_left
-#align nat.coprime.pow_right Nat.coprime.pow_right
-#align nat.coprime.pow Nat.coprime.pow
-#align nat.coprime.eq_one_of_dvd Nat.coprime.eq_one_of_dvd
+#align nat.coprime.pow_left Nat.Coprime.pow_left
+#align nat.coprime.pow_right Nat.Coprime.pow_right
+#align nat.coprime.pow Nat.Coprime.pow
+#align nat.coprime.eq_one_of_dvd Nat.Coprime.eq_one_of_dvd
 #align nat.gcd_mul_dvd_mul_gcd Nat.gcd_mul_dvd_mul_gcd
-#align nat.coprime.gcd_mul Nat.coprime.gcd_mul
+#align nat.coprime.gcd_mul Nat.Coprime.gcd_mul
 #align nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul
diff --git a/Mathlib/Lean/CoreM.lean b/Mathlib/Lean/CoreM.lean
index a269a46054221..5c33e15999c4c 100644
--- a/Mathlib/Lean/CoreM.lean
+++ b/Mathlib/Lean/CoreM.lean
@@ -17,7 +17,7 @@ open Lean Core
 /--
 Run a `CoreM α` in a fresh `Environment` with specified `modules : List Name` imported.
 -/
-def CoreM.withImportModules (modules : List Name) (run : CoreM α)
+def CoreM.withImportModules (modules : Array Name) (run : CoreM α)
     (searchPath : Option SearchPath := none) (options : Options := {})
     (trustLevel : UInt32 := 0) (fileName := "") :
     IO α := unsafe do
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
index 90f483f1ba119..610832b45c5ac 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -592,7 +592,7 @@ end Pdiv
 
 /-- Multiplicative functions -/
 def IsMultiplicative [MonoidWithZero R] (f : ArithmeticFunction R) : Prop :=
-  f 1 = 1 ∧ ∀ {m n : ℕ}, m.coprime n → f (m * n) = f m * f n
+  f 1 = 1 ∧ ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
 #align nat.arithmetic_function.is_multiplicative Nat.ArithmeticFunction.IsMultiplicative
 
 namespace IsMultiplicative
@@ -608,19 +608,19 @@ theorem map_one {f : ArithmeticFunction R} (h : f.IsMultiplicative) : f 1 = 1 :=
 
 @[simp]
 theorem map_mul_of_coprime {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ}
-    (h : m.coprime n) : f (m * n) = f m * f n :=
+    (h : m.Coprime n) : f (m * n) = f m * f n :=
   hf.2 h
 #align nat.arithmetic_function.is_multiplicative.map_mul_of_coprime Nat.ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
 
 end MonoidWithZero
 
 theorem map_prod {ι : Type*} [CommMonoidWithZero R] (g : ι → ℕ) {f : Nat.ArithmeticFunction R}
-    (hf : f.IsMultiplicative) (s : Finset ι) (hs : (s : Set ι).Pairwise (coprime on g)) :
+    (hf : f.IsMultiplicative) (s : Finset ι) (hs : (s : Set ι).Pairwise (Coprime on g)) :
     f (∏ i in s, g i) = ∏ i in s, f (g i) := by
   classical
     induction' s using Finset.induction_on with a s has ih hs
     · simp [hf]
-    rw [coe_insert, Set.pairwise_insert_of_symmetric (coprime.symmetric.comap g)] at hs
+    rw [coe_insert, Set.pairwise_insert_of_symmetric (Coprime.symmetric.comap g)] at hs
     rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
     exact Nat.coprime_prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm
 #align nat.arithmetic_function.is_multiplicative.map_prod Nat.ArithmeticFunction.IsMultiplicative.map_prod
@@ -729,7 +729,7 @@ theorem multiplicative_factorization [CommMonoidWithZero R] (f : ArithmeticFunct
 /-- A recapitulation of the definition of multiplicative that is simpler for proofs -/
 theorem iff_ne_zero [MonoidWithZero R] {f : ArithmeticFunction R} :
     IsMultiplicative f ↔
-      f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.coprime n → f (m * n) = f m * f n := by
+      f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n := by
   refine' and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => _⟩)
   rcases eq_or_ne m 0 with (rfl | hm)
   · simp
diff --git a/Mathlib/NumberTheory/FermatPsp.lean b/Mathlib/NumberTheory/FermatPsp.lean
index 8622e4ca2bcf6..a00b47c3dbadd 100644
--- a/Mathlib/NumberTheory/FermatPsp.lean
+++ b/Mathlib/NumberTheory/FermatPsp.lean
@@ -73,7 +73,7 @@ instance decidablePsp (n b : ℕ) : Decidable (FermatPsp n b) :=
 `n` and `b` are both positive.
 -/
 theorem coprime_of_probablePrime {n b : ℕ} (h : ProbablePrime n b) (h₁ : 1 ≤ n) (h₂ : 1 ≤ b) :
-    Nat.coprime n b := by
+    Nat.Coprime n b := by
   by_cases h₃ : 2 ≤ n
   · -- To prove that `n` is coprime with `b`, we need to show that for all prime factors of `n`,
     -- we can derive a contradiction if `n` divides `b`.
@@ -117,7 +117,7 @@ positive.
 
 This lemma is a small wrapper based on `coprime_of_probablePrime`
 -/
-theorem coprime_of_fermatPsp {n b : ℕ} (h : FermatPsp n b) (h₁ : 1 ≤ b) : Nat.coprime n b := by
+theorem coprime_of_fermatPsp {n b : ℕ} (h : FermatPsp n b) (h₁ : 1 ≤ b) : Nat.Coprime n b := by
   rcases h with ⟨hp, _, hn₂⟩
   exact coprime_of_probablePrime hp (by linarith) h₁
 #align fermat_psp.coprime_of_fermat_psp Nat.coprime_of_fermatPsp
@@ -244,7 +244,7 @@ private theorem psp_from_prime_psp {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_p
   -- to prove this.
   have ha₃ : p ∣ b ^ (p - 1) - 1 := by
     have : ¬p ∣ b := mt (fun h : p ∣ b => dvd_mul_of_dvd_left h _) not_dvd
-    have : p.coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this
+    have : p.Coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this
     have : IsCoprime (b : ℤ) ↑p := this.symm.isCoprime
     have : ↑b ^ (p - 1) ≡ 1 [ZMOD ↑p] := Int.ModEq.pow_card_sub_one_eq_one p_prime this
     have : ↑p ∣ ↑b ^ (p - 1) - ↑1 := by exact_mod_cast Int.ModEq.dvd (Int.ModEq.symm this)
@@ -266,12 +266,12 @@ private theorem psp_from_prime_psp {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_p
     -- We already proved that `b ^ 2 - 1 ∣ b ^ (p - 1) - 1`.
     -- Since `2 ∣ b ^ p + b` and `p ∣ b ^ p + b`, if we show that 2 and p are coprime, then we
     -- know that `2 * p ∣ b ^ p + b`
-    have q₁ : Nat.coprime p (b ^ 2 - 1) :=
+    have q₁ : Nat.Coprime p (b ^ 2 - 1) :=
       haveI q₂ : ¬p ∣ b ^ 2 - 1 := by
         rw [mul_comm] at not_dvd
         exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd
       (Nat.Prime.coprime_iff_not_dvd p_prime).mpr q₂
-    have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ ha₄
+    have q₂ : p * (b ^ 2 - 1) ∣ b ^ (p - 1) - 1 := Nat.Coprime.mul_dvd_of_dvd_of_dvd q₁ ha₃ ha₄
     have q₃ : p * (b ^ 2 - 1) * 2 ∣ (b ^ (p - 1) - 1) * (b ^ p + b) := mul_dvd_mul q₂ ha₂
     have q₄ : p * (b ^ 2 - 1) * 2 ∣ b * ((b ^ (p - 1) - 1) * (b ^ p + b)) :=
       dvd_mul_of_dvd_right q₃ _
diff --git a/Mathlib/NumberTheory/FrobeniusNumber.lean b/Mathlib/NumberTheory/FrobeniusNumber.lean
index e39d94fbecb0f..93e87d1ba6530 100644
--- a/Mathlib/NumberTheory/FrobeniusNumber.lean
+++ b/Mathlib/NumberTheory/FrobeniusNumber.lean
@@ -53,7 +53,7 @@ variable {m n : ℕ}
 
 /-- The **Chicken McNugget theorem** stating that the Frobenius number
   of positive numbers `m` and `n` is `m * n - m - n`. -/
-theorem frobeniusNumber_pair (cop : coprime m n) (hm : 1 < m) (hn : 1 < n) :
+theorem frobeniusNumber_pair (cop : Coprime m n) (hm : 1 < m) (hn : 1 < n) :
     FrobeniusNumber (m * n - m - n) {m, n} := by
   simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]
   have hmn : m + n ≤ m * n := add_le_mul hm hn
diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean
index ecc6fd8be852d..e7dfb9fa4565b 100644
--- a/Mathlib/NumberTheory/NumberField/Units.lean
+++ b/Mathlib/NumberTheory/NumberField/Units.lean
@@ -124,7 +124,7 @@ def torsionOrder [NumberField K] : ℕ+ := ⟨Fintype.card (torsion K), Fintype.
 
 /-- If `k` does not divide `torsionOrder` then there are no nontrivial roots of unity of
   order dividing `k`. -/
-theorem rootsOfUnity_eq_one [NumberField K] {k : ℕ+} (hc : Nat.coprime k (torsionOrder K)) :
+theorem rootsOfUnity_eq_one [NumberField K] {k : ℕ+} (hc : Nat.Coprime k (torsionOrder K)) :
     ζ ∈ rootsOfUnity k (𝓞 K) ↔ ζ = 1 := by
   rw [mem_rootsOfUnity]
   refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean
index c6186e5cb15a5..e39110d8d95c4 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -487,7 +487,7 @@ protected theorem div_pow (dvd : p ^ a ∣ b) : padicValNat p (b / p ^ a) = padi
   rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]
 #align padic_val_nat.div_pow padicValNat.div_pow
 
-protected theorem div' {m : ℕ} (cpm : coprime p m) {b : ℕ} (dvd : m ∣ b) :
+protected theorem div' {m : ℕ} (cpm : Coprime p m) {b : ℕ} (dvd : m ∣ b) :
     padicValNat p (b / m) = padicValNat p b := by
   rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
     Nat.sub_zero]
diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean
index 1e8c5bffb7d64..f1d79ad8056cd 100644
--- a/Mathlib/NumberTheory/Padics/RingHoms.lean
+++ b/Mathlib/NumberTheory/Padics/RingHoms.lean
@@ -109,10 +109,10 @@ theorem norm_sub_modPart_aux (r : ℚ) (h : ‖(r : ℚ_[p])‖ ≤ 1) :
     Int.cast_mul, zero_mul, add_zero] at this
   push_cast
   rw [mul_right_comm, mul_assoc, ← this]
-  suffices rdcp : r.den.coprime p
+  suffices rdcp : r.den.Coprime p
   · rw [rdcp.gcd_eq_one]
     simp only [mul_one, cast_one, sub_self]
-  apply coprime.symm
+  apply Coprime.symm
   apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right
   rw [← Int.coe_nat_dvd, ← norm_int_lt_one_iff_dvd, not_lt]
   apply ge_of_eq
diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean
index fc4135462a62e..9e30cdedc9c99 100644
--- a/Mathlib/NumberTheory/PellMatiyasevic.lean
+++ b/Mathlib/NumberTheory/PellMatiyasevic.lean
@@ -391,7 +391,7 @@ theorem yz_sub {m n} (h : n ≤ m) : yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m
   exact congr_arg Zsqrtd.im (pellZd_sub a1 h)
 #align pell.yz_sub Pell.yz_sub
 
-theorem xy_coprime (n) : (xn a1 n).coprime (yn a1 n) :=
+theorem xy_coprime (n) : (xn a1 n).Coprime (yn a1 n) :=
   Nat.coprime_of_dvd' fun k _ kx ky => by
     let p := pell_eq a1 n
     rw [← p]
@@ -436,8 +436,8 @@ theorem y_dvd_iff (m n) : yn a1 m ∣ yn a1 n ↔ m ∣ n :=
   ⟨fun h =>
     Nat.dvd_of_mod_eq_zero <|
       (Nat.eq_zero_or_pos _).resolve_right fun hp => by
-        have co : Nat.coprime (yn a1 m) (xn a1 (m * (n / m))) :=
-          Nat.coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))
+        have co : Nat.Coprime (yn a1 m) (xn a1 (m * (n / m))) :=
+          Nat.Coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))
         have m0 : 0 < m :=
           m.eq_zero_or_pos.resolve_left fun e => by
             rw [e, Nat.mod_zero] at hp;rw [e] at h
@@ -855,10 +855,10 @@ theorem matiyasevic {a k x y} :
       let v := yn a1 m
       have ky : k ≤ y := yn_ge_n a1 k
       have yv : y * y ∣ v := (ysq_dvd_yy a1 k).trans <| (y_dvd_iff _ _ _).2 <| dvd_mul_left _ _
-      have uco : Nat.coprime u (4 * y) :=
+      have uco : Nat.Coprime u (4 * y) :=
         have : 2 ∣ v :=
           modEq_zero_iff_dvd.1 <| (yn_modEq_two _ _).trans (dvd_mul_right _ _).modEq_zero_nat
-        have : Nat.coprime u 2 := (xy_coprime a1 m).coprime_dvd_right this
+        have : Nat.Coprime u 2 := (xy_coprime a1 m).coprime_dvd_right this
         (this.mul_right this).mul_right <|
           (xy_coprime _ _).coprime_dvd_right (dvd_of_mul_left_dvd yv)
       let ⟨b, ba, bm1⟩ := chineseRemainder uco a 1
diff --git a/Mathlib/NumberTheory/PrimeCounting.lean b/Mathlib/NumberTheory/PrimeCounting.lean
index 20c8927a39601..f8e9b88dead43 100644
--- a/Mathlib/NumberTheory/PrimeCounting.lean
+++ b/Mathlib/NumberTheory/PrimeCounting.lean
@@ -85,7 +85,7 @@ theorem primeCounting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
       apply card_union_le
     _ ≤ π' k + ((Ico k (k + n)).filter Prime).card := by
       rw [primeCounting', count_eq_card_filter_range]
-    _ ≤ π' k + ((Ico k (k + n)).filter (coprime a)).card := by
+    _ ≤ π' k + ((Ico k (k + n)).filter (Coprime a)).card := by
       refine' add_le_add_left (card_le_of_subset _) k.primeCounting'
       simp only [subset_iff, and_imp, mem_filter, mem_Ico]
       intro p succ_k_le_p p_lt_n p_prime
diff --git a/Mathlib/NumberTheory/SumTwoSquares.lean b/Mathlib/NumberTheory/SumTwoSquares.lean
index 0840e85e4988f..4936e6c381629 100644
--- a/Mathlib/NumberTheory/SumTwoSquares.lean
+++ b/Mathlib/NumberTheory/SumTwoSquares.lean
@@ -82,7 +82,7 @@ theorem ZMod.isSquare_neg_one_of_dvd {m n : ℕ} (hd : m ∣ n) (hs : IsSquare (
 
 /-- If `-1` is a square modulo coprime natural numbers `m` and `n`, then `-1` is also
 a square modulo `m*n`. -/
-theorem ZMod.isSquare_neg_one_mul {m n : ℕ} (hc : m.coprime n) (hm : IsSquare (-1 : ZMod m))
+theorem ZMod.isSquare_neg_one_mul {m n : ℕ} (hc : m.Coprime n) (hm : IsSquare (-1 : ZMod m))
     (hn : IsSquare (-1 : ZMod n)) : IsSquare (-1 : ZMod (m * n)) := by
   have : IsSquare (-1 : ZMod m × ZMod n) := by
     rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
@@ -111,7 +111,7 @@ theorem ZMod.isSquare_neg_one_iff {n : ℕ} (hn : Squarefree n) :
   · exact False.elim (hn.ne_zero rfl)
   · exact ⟨0, by simp only [Fin.zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩
   · haveI : Fact p.Prime := ⟨hpp⟩
-    have hcp : p.coprime n := by
+    have hcp : p.Coprime n := by
       by_contra hc
       exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
     have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr (H hpp (dvd_mul_right p n))
@@ -174,7 +174,7 @@ theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime {n x y : ℤ} (h : n
 /-- If the natural number `n` is a sum of two squares of coprime natural numbers, then
 `-1` is a square modulo `n`. -/
 theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime {n x y : ℕ} (h : n = x ^ 2 + y ^ 2)
-    (hc : x.coprime y) : IsSquare (-1 : ZMod n) := by
+    (hc : x.Coprime y) : IsSquare (-1 : ZMod n) := by
   zify at h
   exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime
 #align zmod.is_square_neg_one_of_eq_sq_add_sq_of_coprime ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime
diff --git a/Mathlib/NumberTheory/WellApproximable.lean b/Mathlib/NumberTheory/WellApproximable.lean
index ded787e352f1e..5ba1100193d69 100644
--- a/Mathlib/NumberTheory/WellApproximable.lean
+++ b/Mathlib/NumberTheory/WellApproximable.lean
@@ -105,7 +105,7 @@ namespace approxOrderOf
 variable {A : Type*} [SeminormedCommGroup A] {a : A} {m n : ℕ} (δ : ℝ)
 
 @[to_additive]
-theorem image_pow_subset_of_coprime (hm : 0 < m) (hmn : n.coprime m) :
+theorem image_pow_subset_of_coprime (hm : 0 < m) (hmn : n.Coprime m) :
     (fun (y : A) => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (m * δ) := by
   rintro - ⟨a, ha, rfl⟩
   obtain ⟨b, hb, hab⟩ := mem_approxOrderOf_iff.mp ha
@@ -131,7 +131,7 @@ theorem image_pow_subset (n : ℕ) (hm : 0 < m) :
 #align approx_add_order_of.image_nsmul_subset approxAddOrderOf.image_nsmul_subset
 
 @[to_additive]
-theorem smul_subset_of_coprime (han : (orderOf a).coprime n) :
+theorem smul_subset_of_coprime (han : (orderOf a).Coprime n) :
     a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ := by
   simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
     smul_ball'', smul_eq_mul, mem_setOf_eq]
@@ -287,7 +287,7 @@ theorem addWellApproximable_ae_empty_or_univ (δ : ℕ → ℝ) (hδ : Tendsto 
         (Nat.cast_pos.mpr hp.pos) _ hδ
     refine' (SupHom.apply_blimsup_le (sSupHom.setImage f)).trans (mono_blimsup _)
     rintro n ⟨hn, h_div, h_ndiv⟩
-    have h_cop : (addOrderOf x).coprime (n / p) := by
+    have h_cop : (addOrderOf x).Coprime (n / p) := by
       obtain ⟨q, rfl⟩ := h_div
       rw [hu₀, Subtype.coe_mk, hp.coprime_iff_not_dvd, q.mul_div_cancel_left hp.pos]
       exact fun contra => h_ndiv (mul_dvd_mul_left p contra)
diff --git a/Mathlib/RingTheory/Coprime/Lemmas.lean b/Mathlib/RingTheory/Coprime/Lemmas.lean
index 9c7d74598cb76..ccc314a6e37ea 100644
--- a/Mathlib/RingTheory/Coprime/Lemmas.lean
+++ b/Mathlib/RingTheory/Coprime/Lemmas.lean
@@ -39,18 +39,18 @@ theorem Int.isCoprime_iff_gcd_eq_one {m n : ℤ} : IsCoprime m n ↔ Int.gcd m n
     intro h
     exact ⟨_, _, h⟩
 
-theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.coprime m n := by
+theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.Coprime m n := by
   rw [Int.isCoprime_iff_gcd_eq_one, Int.coe_nat_gcd]
 #align nat.is_coprime_iff_coprime Nat.isCoprime_iff_coprime
 
-alias ⟨IsCoprime.nat_coprime, Nat.coprime.isCoprime⟩ := Nat.isCoprime_iff_coprime
+alias ⟨IsCoprime.nat_coprime, Nat.Coprime.isCoprime⟩ := Nat.isCoprime_iff_coprime
 #align is_coprime.nat_coprime IsCoprime.nat_coprime
-#align nat.coprime.is_coprime Nat.coprime.isCoprime
+#align nat.coprime.is_coprime Nat.Coprime.isCoprime
 
 theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ}
-    (h : Nat.coprime a b) : (a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
+    (h : Nat.Coprime a b) : (a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
   IsCoprime.ne_zero_or_ne_zero (R := A) <| by
-    simpa only [map_natCast] using IsCoprime.map (Nat.coprime.isCoprime h) (Int.castRingHom A)
+    simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)
 
 theorem IsCoprime.prod_left : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x :=
   Finset.induction_on t (fun _ ↦ isCoprime_one_left) fun b t hbt ih H ↦ by
diff --git a/Mathlib/RingTheory/Int/Basic.lean b/Mathlib/RingTheory/Int/Basic.lean
index 98f5e525eb155..1fad6d1dc062d 100644
--- a/Mathlib/RingTheory/Int/Basic.lean
+++ b/Mathlib/RingTheory/Int/Basic.lean
@@ -199,7 +199,7 @@ theorem gcd_eq_one_iff_coprime {a b : ℤ} : Int.gcd a b = 1 ↔ IsCoprime a b :
     exact dvd_add ((coe_nat_dvd_left.mpr ha).mul_left _) ((coe_nat_dvd_left.mpr hb).mul_left _)
 #align int.gcd_eq_one_iff_coprime Int.gcd_eq_one_iff_coprime
 
-theorem coprime_iff_nat_coprime {a b : ℤ} : IsCoprime a b ↔ Nat.coprime a.natAbs b.natAbs := by
+theorem coprime_iff_nat_coprime {a b : ℤ} : IsCoprime a b ↔ Nat.Coprime a.natAbs b.natAbs := by
   rw [← gcd_eq_one_iff_coprime, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]
 #align int.coprime_iff_nat_coprime Int.coprime_iff_nat_coprime
 
diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean
index bf2a5cf144ee1..4fd198ee87b63 100644
--- a/Mathlib/RingTheory/Multiplicity.lean
+++ b/Mathlib/RingTheory/Multiplicity.lean
@@ -647,13 +647,13 @@ section Nat
 open multiplicity
 
 theorem multiplicity_eq_zero_of_coprime {p a b : ℕ} (hp : p ≠ 1)
-    (hle : multiplicity p a ≤ multiplicity p b) (hab : Nat.coprime a b) : multiplicity p a = 0 := by
+    (hle : multiplicity p a ≤ multiplicity p b) (hab : Nat.Coprime a b) : multiplicity p a = 0 := by
   rw [multiplicity_le_multiplicity_iff] at hle
   rw [← nonpos_iff_eq_zero, ← not_lt, PartENat.pos_iff_one_le, ← Nat.cast_one, ←
     pow_dvd_iff_le_multiplicity]
   intro h
   have := Nat.dvd_gcd h (hle _ h)
-  rw [coprime.gcd_eq_one hab, Nat.dvd_one, pow_one] at this
+  rw [Coprime.gcd_eq_one hab, Nat.dvd_one, pow_one] at this
   exact hp this
 #align multiplicity_eq_zero_of_coprime multiplicity_eq_zero_of_coprime
 
diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
index d85c79681ce75..eaf8baa00d67c 100644
--- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
+++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
@@ -615,8 +615,8 @@ theorem cyclotomic_coeff_zero (R : Type*) [CommRing R] {n : ℕ} (hn : 1 < n) :
 /-- If `(a : ℕ)` is a root of `cyclotomic n (ZMod p)`, where `p` is a prime, then `a` and `p` are
 coprime. -/
 theorem coprime_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : Fact p.Prime] {a : ℕ}
-    (hroot : IsRoot (cyclotomic n (ZMod p)) (Nat.castRingHom (ZMod p) a)) : a.coprime p := by
-  apply Nat.coprime.symm
+    (hroot : IsRoot (cyclotomic n (ZMod p)) (Nat.castRingHom (ZMod p) a)) : a.Coprime p := by
+  apply Nat.Coprime.symm
   rw [hprime.1.coprime_iff_not_dvd]
   intro h
   replace h := (ZMod.nat_cast_zmod_eq_zero_iff_dvd a p).2 h
diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean
index 565de5ce40de5..06812d7677ac5 100644
--- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean
+++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean
@@ -410,7 +410,7 @@ theorem coe_units_iff {ζ : Mˣ} : IsPrimitiveRoot (ζ : M) k ↔ IsPrimitiveRoo
 #align is_primitive_root.coe_units_iff IsPrimitiveRoot.coe_units_iff
 
 -- Porting note `variable` above already contains `(h : IsPrimitiveRoot ζ k)`
-theorem pow_of_coprime (i : ℕ) (hi : i.coprime k) : IsPrimitiveRoot (ζ ^ i) k := by
+theorem pow_of_coprime (i : ℕ) (hi : i.Coprime k) : IsPrimitiveRoot (ζ ^ i) k := by
   by_cases h0 : k = 0
   · subst k; simp_all only [pow_one, Nat.coprime_zero_right]
   rcases h.isUnit (Nat.pos_of_ne_zero h0) with ⟨ζ, rfl⟩
@@ -432,7 +432,7 @@ theorem pow_of_prime (h : IsPrimitiveRoot ζ k) {p : ℕ} (hprime : Nat.Prime p)
 #align is_primitive_root.pow_of_prime IsPrimitiveRoot.pow_of_prime
 
 theorem pow_iff_coprime (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ℕ) :
-    IsPrimitiveRoot (ζ ^ i) k ↔ i.coprime k := by
+    IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k := by
   refine' ⟨_, h.pow_of_coprime i⟩
   intro hi
   obtain ⟨a, ha⟩ := i.gcd_dvd_left k
@@ -440,7 +440,7 @@ theorem pow_iff_coprime (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ℕ) :
   suffices b = k by
     -- Porting note: was `rwa [this, ← one_mul k, mul_left_inj' h0.ne', eq_comm] at hb`
     rw [this, eq_comm, Nat.mul_left_eq_self_iff h0] at hb
-    rwa [Nat.coprime]
+    rwa [Nat.Coprime]
   rw [ha] at hi
   rw [mul_comm] at hb
   apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _)
@@ -774,7 +774,7 @@ theorem eq_pow_of_pow_eq_one {k : ℕ} {ζ ξ : R} (h : IsPrimitiveRoot ζ k) (h
 #align is_primitive_root.eq_pow_of_pow_eq_one IsPrimitiveRoot.eq_pow_of_pow_eq_one
 
 theorem isPrimitiveRoot_iff' {k : ℕ+} {ζ ξ : Rˣ} (h : IsPrimitiveRoot ζ k) :
-    IsPrimitiveRoot ξ k ↔ ∃ i < (k : ℕ), i.coprime k ∧ ζ ^ i = ξ := by
+    IsPrimitiveRoot ξ k ↔ ∃ i < (k : ℕ), i.Coprime k ∧ ζ ^ i = ξ := by
   constructor
   · intro hξ
     obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one
@@ -784,7 +784,7 @@ theorem isPrimitiveRoot_iff' {k : ℕ+} {ζ ξ : Rˣ} (h : IsPrimitiveRoot ζ k)
 #align is_primitive_root.is_primitive_root_iff' IsPrimitiveRoot.isPrimitiveRoot_iff'
 
 theorem isPrimitiveRoot_iff {k : ℕ} {ζ ξ : R} (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) :
-    IsPrimitiveRoot ξ k ↔ ∃ i < k, i.coprime k ∧ ζ ^ i = ξ := by
+    IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ := by
   constructor
   · intro hξ
     obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_pow_eq_one hξ.pow_eq_one h0
diff --git a/Mathlib/RingTheory/RootsOfUnity/Complex.lean b/Mathlib/RingTheory/RootsOfUnity/Complex.lean
index 1c45dfe9713a8..e79317a19897c 100644
--- a/Mathlib/RingTheory/RootsOfUnity/Complex.lean
+++ b/Mathlib/RingTheory/RootsOfUnity/Complex.lean
@@ -29,7 +29,7 @@ open Polynomial Real
 
 open scoped Nat Real
 
-theorem isPrimitiveRoot_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.coprime n) :
+theorem isPrimitiveRoot_exp_of_coprime (i n : ℕ) (h0 : n ≠ 0) (hi : i.Coprime n) :
     IsPrimitiveRoot (exp (2 * π * I * (i / n))) n := by
   rw [IsPrimitiveRoot.iff_def]
   simp only [← exp_nat_mul, exp_eq_one_iff]
@@ -55,7 +55,7 @@ theorem isPrimitiveRoot_exp (n : ℕ) (h0 : n ≠ 0) : IsPrimitiveRoot (exp (2 *
 #align complex.is_primitive_root_exp Complex.isPrimitiveRoot_exp
 
 theorem isPrimitiveRoot_iff (ζ : ℂ) (n : ℕ) (hn : n ≠ 0) :
-    IsPrimitiveRoot ζ n ↔ ∃ i < (n : ℕ), ∃ _ : i.coprime n, exp (2 * π * I * (i / n)) = ζ := by
+    IsPrimitiveRoot ζ n ↔ ∃ i < (n : ℕ), ∃ _ : i.Coprime n, exp (2 * π * I * (i / n)) = ζ := by
   have hn0 : (n : ℂ) ≠ 0 := by exact_mod_cast hn
   constructor; swap
   · rintro ⟨i, -, hi, rfl⟩; exact isPrimitiveRoot_exp_of_coprime i n hn hi
diff --git a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
index 23b5d58850ee1..b85cc3358a31f 100644
--- a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
+++ b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
@@ -172,7 +172,7 @@ theorem minpoly_eq_pow {p : ℕ} [hprime : Fact p.Prime] (hdiv : ¬p ∣ n) :
 /-- If `m : ℕ` is coprime with `n`,
 then the minimal polynomials of a primitive `n`-th root of unity `μ`
 and of `μ ^ m` are the same. -/
-theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.coprime m n) :
+theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.Coprime m n) :
     minpoly ℤ μ = minpoly ℤ (μ ^ m) := by
   revert n hcop
   refine' UniqueFactorizationMonoid.induction_on_prime m _ _ _
@@ -184,11 +184,11 @@ theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.coprime m n) :
     simp [Nat.isUnit_iff.mp hunit]
   · intro a p _ hprime
     intro hind h hcop
-    rw [hind h (Nat.coprime.coprime_mul_left hcop)]; clear hind
+    rw [hind h (Nat.Coprime.coprime_mul_left hcop)]; clear hind
     replace hprime := hprime.nat_prime
-    have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.coprime.coprime_mul_right hcop)
+    have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)
     haveI := Fact.mk hprime
-    rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.coprime.coprime_mul_left hcop)) hdiv]
+    rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.Coprime.coprime_mul_left hcop)) hdiv]
     congr 1
     ring
 #align is_primitive_root.minpoly_eq_pow_coprime IsPrimitiveRoot.minpoly_eq_pow_coprime
@@ -196,7 +196,7 @@ theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.coprime m n) :
 /-- If `m : ℕ` is coprime with `n`,
 then the minimal polynomial of a primitive `n`-th root of unity `μ`
 has `μ ^ m` as root. -/
-theorem pow_isRoot_minpoly {m : ℕ} (hcop : Nat.coprime m n) :
+theorem pow_isRoot_minpoly {m : ℕ} (hcop : Nat.Coprime m n) :
     IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m) := by
   simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]
   exact minpoly.aeval ℤ (μ ^ m)
diff --git a/Mathlib/Tactic/NthRewrite.lean b/Mathlib/Tactic/NthRewrite.lean
index 16da418fc1560..840b98377dd0b 100644
--- a/Mathlib/Tactic/NthRewrite.lean
+++ b/Mathlib/Tactic/NthRewrite.lean
@@ -18,30 +18,6 @@ namespace Mathlib.Tactic
 
 open Lean Elab Tactic Meta Parser.Tactic
 
-/-- Variant of `rewriteTarget` that allows to use `Occurrences`.
-
-This def should be in Core. -/
-def rewriteTarget' (stx : Syntax) (symm : Bool) (occs : Occurrences := Occurrences.all)
-    (config : Rewrite.Config := { : Rewrite.Config }) : TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    let r ← (← getMainGoal).rewrite (← getMainTarget) e symm occs config
-    let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
-    replaceMainGoal (mvarId' :: r.mvarIds)
-
-/-- Variant of `rewriteLocalDecl` that allows to use `Occurrences`.
-
-This def should be in Core. -/
-def rewriteLocalDecl' (stx : Syntax) (symm : Bool) (fvarId : FVarId)
-    (occs : Occurrences := Occurrences.all) (config : Rewrite.Config := { : Rewrite.Config }) :
-    TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    let localDecl ← fvarId.getDecl
-    let rwResult ← (← getMainGoal).rewrite localDecl.type e symm occs config
-    let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
-    replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
-
 /-- `nth_rewrite` is a variant of `rewrite` that only changes the nth occurrence of the expression
 to be rewritten.
 
@@ -57,10 +33,11 @@ syntax (name := nthRewriteSeq) "nth_rewrite" (config)? ppSpace num rwRuleSeq (lo
     let cfg ← elabRewriteConfig stx[1]
     let loc := expandOptLocation stx[4]
     let occ := Occurrences.pos [n.getNat]
+    let cfg := { cfg with occs := occ }
     withRWRulesSeq stx[0] stx[3] fun symm term => do
       withLocation loc
-        (rewriteLocalDecl' term symm · occ cfg)
-        (rewriteTarget' term symm occ cfg)
+        (rewriteLocalDecl term symm · cfg)
+        (rewriteTarget term symm cfg)
         (throwTacticEx `nth_rewrite · "did not find instance of the pattern in the current goal")
   | _ => throwUnsupportedSyntax
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 17a199a57cb56..2f083dcf29339 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -36,7 +36,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323",
+    "rev": "80089ff4cd1808ad1506a62dac557517d9b875ff",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
diff --git a/lakefile.lean b/lakefile.lean
index aba9e8e261859..fe6a95fe1d11e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -29,8 +29,11 @@ lean_lib Mathlib where
   moreLeanArgs := moreLeanArgs
   weakLeanArgs := weakLeanArgs
 
-lean_exe runLinter where
-  root := `scripts.runLinter
+-- Due to a change in Lake at v4.1.0-rc1, we need to give this a different name
+-- than the `lean_exe runLinter` inherited from Std, or we always run that.
+-- See https://github.com/leanprover/lean4/issues/2548
+lean_exe runMathlibLinter where
+  root := `scripts.runMathlibLinter
   supportInterpreter := true
 
 lean_exe checkYaml where
diff --git a/lean-toolchain b/lean-toolchain
index f0a6d660f08ad..640f2091db69e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.1.0-rc1
diff --git a/scripts/checkYaml.lean b/scripts/checkYaml.lean
index 88fc37f2cf3b0..4b44bd540eda8 100644
--- a/scripts/checkYaml.lean
+++ b/scripts/checkYaml.lean
@@ -43,7 +43,7 @@ def processDb (decls : ConstMap) : String × String → IO Bool
     return false
 
 unsafe def main : IO Unit := do
-  CoreM.withImportModules [`Mathlib]
+  CoreM.withImportModules #[`Mathlib]
       (searchPath := compile_time_search_path%) (trustLevel := 1024) do
     let decls := (←getEnv).constants
     let results ← databases.mapM (fun p => processDb decls p)
diff --git a/scripts/runLinter.lean b/scripts/runMathlibLinter.lean
similarity index 93%
rename from scripts/runLinter.lean
rename to scripts/runMathlibLinter.lean
index db07a76ae4011..c43198c85f352 100644
--- a/scripts/runLinter.lean
+++ b/scripts/runMathlibLinter.lean
@@ -23,10 +23,10 @@ unsafe def main (args : List String) : IO Unit := do
       | [] => some `Mathlib
       | [mod] => Syntax.decodeNameLit s!"`{mod}"
       | _ => none
-    | IO.eprintln "Usage: runLinter [--update] [Mathlib.Data.Nat]" *> IO.Process.exit 1
+    | IO.eprintln "Usage: runMathlibLinter [--update] [Mathlib.Data.Nat.Basic]" *> IO.Process.exit 1
   let nolintsFile := "scripts/nolints.json"
   let nolints ← readJsonFile NoLints nolintsFile
-  CoreM.withImportModules [module]
+  CoreM.withImportModules #[module]
       (searchPath := compile_time_search_path%) (trustLevel := 1024) do
     let decls ← getDeclsInPackage `Mathlib
     let linters ← getChecks (slow := true) (useOnly := false)
diff --git a/test/norm_num_ext.lean b/test/norm_num_ext.lean
index 9770c1e17858e..e1cccc8619ce4 100644
--- a/test/norm_num_ext.lean
+++ b/test/norm_num_ext.lean
@@ -39,14 +39,14 @@ example : Nat.sqrt 122 = 11 := by norm_num1
 example : Nat.sqrt (123456^2) = 123456 := by norm_num1
 example : Nat.sqrt (123456^2 + 123456) = 123456 := by norm_num1
 
-theorem ex11 : Nat.coprime 1 2 := by norm_num1
-theorem ex12 : Nat.coprime 2 1 := by norm_num1
-theorem ex13 : ¬ Nat.coprime 0 0 := by norm_num1
-theorem ex14 : ¬ Nat.coprime 0 3 := by norm_num1
-theorem ex15 : ¬ Nat.coprime 2 0 := by norm_num1
-theorem ex16 : Nat.coprime 2 3 := by norm_num1
-theorem ex16' : Nat.coprime 3 2 := by norm_num1
-theorem ex17 : ¬ Nat.coprime 2 4 := by norm_num1
+theorem ex11 : Nat.Coprime 1 2 := by norm_num1
+theorem ex12 : Nat.Coprime 2 1 := by norm_num1
+theorem ex13 : ¬ Nat.Coprime 0 0 := by norm_num1
+theorem ex14 : ¬ Nat.Coprime 0 3 := by norm_num1
+theorem ex15 : ¬ Nat.Coprime 2 0 := by norm_num1
+theorem ex16 : Nat.Coprime 2 3 := by norm_num1
+theorem ex16' : Nat.Coprime 3 2 := by norm_num1
+theorem ex17 : ¬ Nat.Coprime 2 4 := by norm_num1
 
 theorem ex21 : Nat.gcd 1 2 = 1 := by norm_num1
 theorem ex22 : Nat.gcd 2 1 = 1 := by norm_num1
@@ -128,61 +128,61 @@ example : Nat.gcd 35 29 = 1 := by norm_num1
 example : Int.gcd 35 29 = 1 := by norm_num1
 example : Nat.lcm 35 29 = 1015 := by norm_num1
 example : Int.gcd 35 29 = 1 := by norm_num1
-example : Nat.coprime 35 29 := by norm_num1
+example : Nat.Coprime 35 29 := by norm_num1
 
 example : Nat.gcd 80 2 = 2 := by norm_num1
 example : Int.gcd 80 2 = 2 := by norm_num1
 example : Nat.lcm 80 2 = 80 := by norm_num1
 example : Int.gcd 80 2 = 2 := by norm_num1
-example : ¬ Nat.coprime 80 2 := by norm_num1
+example : ¬ Nat.Coprime 80 2 := by norm_num1
 
 example : Nat.gcd 19 17 = 1 := by norm_num1
 example : Int.gcd 19 17 = 1 := by norm_num1
 example : Nat.lcm 19 17 = 323 := by norm_num1
 example : Int.gcd 19 17 = 1 := by norm_num1
-example : Nat.coprime 19 17 := by norm_num1
+example : Nat.Coprime 19 17 := by norm_num1
 
 example : Nat.gcd 11 18 = 1 := by norm_num1
 example : Int.gcd 11 18 = 1 := by norm_num1
 example : Nat.lcm 11 18 = 198 := by norm_num1
 example : Int.gcd 11 18 = 1 := by norm_num1
-example : Nat.coprime 11 18 := by norm_num1
+example : Nat.Coprime 11 18 := by norm_num1
 
 example : Nat.gcd 23 73 = 1 := by norm_num1
 example : Int.gcd 23 73 = 1 := by norm_num1
 example : Nat.lcm 23 73 = 1679 := by norm_num1
 example : Int.gcd 23 73 = 1 := by norm_num1
-example : Nat.coprime 23 73 := by norm_num1
+example : Nat.Coprime 23 73 := by norm_num1
 
 example : Nat.gcd 73 68 = 1 := by norm_num1
 example : Int.gcd 73 68 = 1 := by norm_num1
 example : Nat.lcm 73 68 = 4964 := by norm_num1
 example : Int.gcd 73 68 = 1 := by norm_num1
-example : Nat.coprime 73 68 := by norm_num1
+example : Nat.Coprime 73 68 := by norm_num1
 
 example : Nat.gcd 28 16 = 4 := by norm_num1
 example : Int.gcd 28 16 = 4 := by norm_num1
 example : Nat.lcm 28 16 = 112 := by norm_num1
 example : Int.gcd 28 16 = 4 := by norm_num1
-example : ¬ Nat.coprime 28 16 := by norm_num1
+example : ¬ Nat.Coprime 28 16 := by norm_num1
 
 example : Nat.gcd 44 98 = 2 := by norm_num1
 example : Int.gcd 44 98 = 2 := by norm_num1
 example : Nat.lcm 44 98 = 2156 := by norm_num1
 example : Int.gcd 44 98 = 2 := by norm_num1
-example : ¬ Nat.coprime 44 98 := by norm_num1
+example : ¬ Nat.Coprime 44 98 := by norm_num1
 
 example : Nat.gcd 21 79 = 1 := by norm_num1
 example : Int.gcd 21 79 = 1 := by norm_num1
 example : Nat.lcm 21 79 = 1659 := by norm_num1
 example : Int.gcd 21 79 = 1 := by norm_num1
-example : Nat.coprime 21 79 := by norm_num1
+example : Nat.Coprime 21 79 := by norm_num1
 
 example : Nat.gcd 93 34 = 1 := by norm_num1
 example : Int.gcd 93 34 = 1 := by norm_num1
 example : Nat.lcm 93 34 = 3162 := by norm_num1
 example : Int.gcd 93 34 = 1 := by norm_num1
-example : Nat.coprime 93 34 := by norm_num1
+example : Nat.Coprime 93 34 := by norm_num1
 
 example : ¬ Nat.Prime 912 := by norm_num1
 example : Nat.minFac 912 = 2 := by norm_num1