From 43ec3ce46c18c2ad54fb5067f539f273260af786 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 3 Nov 2023 19:29:50 +0000
Subject: [PATCH 1/6] refactor: Unify spelling of "prime factors" mathlib can't
 make up its mind on whether to spell "the prime factors of `n`" as
 `n.factors.toFinset` or `n.factorization.support`, even though those two are
 defeq. This PR proposes to unify everything to a new definition
 `Nat.primeFactors`, and stream the existing scattered API about
 `n.factors.toFinset` and `n.factorization.support` to `Nat.primeFactors`. We
 also get to write a bit more API that didn't make sense before, eg
 `primeFactors_mono`.

---
 Mathlib/Data/Nat/Factorization/Basic.lean    | 152 +++++++++----------
 Mathlib/Data/Nat/Factorization/PrimePow.lean |   9 +-
 Mathlib/Data/Nat/Factors.lean                |   3 +
 Mathlib/Data/Nat/Totient.lean                |  47 +++---
 Mathlib/NumberTheory/MaricaSchoenheim.lean   |  39 +++++
 5 files changed, 144 insertions(+), 106 deletions(-)
 create mode 100644 Mathlib/NumberTheory/MaricaSchoenheim.lean

diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
index 07135e187cf6b..2eeb4972575a3 100644
--- a/Mathlib/Data/Nat/Factorization/Basic.lean
+++ b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -47,22 +47,58 @@ open Nat Finset List Finsupp
 open BigOperators
 
 namespace Nat
+variable {a b m n p : ℕ}
+
+/-- The prime factors of a natural number as a finset. -/
+@[pp_dot] def primeFactors (n : ℕ) : Finset ℕ := n.factors.toFinset
+
+@[simp] lemma toFinset_factors (n : ℕ) : n.factors.toFinset = n.primeFactors := rfl
+
+@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
+  simp_rw [←toFinset_factors, List.mem_toFinset, mem_factors']
+
+lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by
+  simp [hn]
+
+lemma primeFactors_mono (hmn : m ∣ n) (hn : n ≠ 0) : primeFactors m ⊆ primeFactors n := by
+  simp only [subset_iff, mem_primeFactors, and_imp]
+  exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩
+
+lemma mem_primeFactors_iff_mem_factors : p ∈ n.primeFactors ↔ p ∈ n.factors := by
+  simp only [primeFactors, List.mem_toFinset]
+
+lemma prime_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p.Prime := (mem_primeFactors.1 hp).1
+lemma dvd_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p ∣ n := (mem_primeFactors.1 hp).2.1
+
+lemma pos_of_mem_primeFactors (hp : p ∈ n.primeFactors) : 0 < p :=
+  (prime_of_mem_primeFactors hp).pos
+
+lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
+  le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt $ dvd_of_mem_primeFactors h
+
+@[simp] lemma primeFactors_zero : primeFactors 0 = ∅ := rfl
+@[simp] lemma primeFactors_one : primeFactors 0 = ∅ := rfl
+
+lemma primeFactors_mul (ha : a ≠ 0) (hb : b ≠ 0) :
+    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors := by
+  ext
+  simp only [Finset.mem_union, mem_primeFactors_iff_mem_factors, mem_factors_mul ha hb]
+
+lemma primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) :
+    (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors := by
+  ext; simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]; aesop
 
 /-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
  mapping each prime factor of `n` to its multiplicity in `n`. -/
 def factorization (n : ℕ) : ℕ →₀ ℕ where
-  support := n.factors.toFinset
+  support := n.primeFactors
   toFun p := if p.Prime then padicValNat p n else 0
-  mem_support_toFun := by
-    rcases eq_or_ne n 0 with (rfl | hn0)
-    · simp
-    simp only [mem_factors hn0, mem_toFinset, Ne.def, ite_eq_right_iff, not_forall, exists_prop,
-      and_congr_right_iff]
-    rintro p hp
-    haveI := fact_iff.mpr hp
-    exact dvd_iff_padicValNat_ne_zero hn0
+  mem_support_toFun := by simp [not_or]; aesop
 #align nat.factorization Nat.factorization
 
+/-- The support of `n.factorization` is exactly `n.primeFactors`. -/
+@[simp] lemma support_factorization (n : ℕ) : (factorization n).support = n.primeFactors := rfl
+
 theorem factorization_def (n : ℕ) {p : ℕ} (pp : p.Prime) : n.factorization p = padicValNat p n := by
   simpa [factorization] using absurd pp
 #align nat.factorization_def Nat.factorization_def
@@ -122,37 +158,19 @@ theorem factorization_zero : factorization 0 = 0 := by simp [factorization]
 theorem factorization_one : factorization 1 = 0 := by simp [factorization]
 #align nat.factorization_one Nat.factorization_one
 
-/-- The support of `n.factorization` is exactly `n.factors.toFinset` -/
-@[simp]
-theorem support_factorization {n : ℕ} : n.factorization.support = n.factors.toFinset := by
-  simp [factorization]
-#align nat.support_factorization Nat.support_factorization
-
-theorem factor_iff_mem_factorization {n p : ℕ} : p ∈ n.factorization.support ↔ p ∈ n.factors := by
-  simp only [support_factorization, List.mem_toFinset]
-#align nat.factor_iff_mem_factorization Nat.factor_iff_mem_factorization
-
-theorem prime_of_mem_factorization {n p : ℕ} (hp : p ∈ n.factorization.support) : p.Prime :=
-  prime_of_mem_factors (factor_iff_mem_factorization.mp hp)
-#align nat.prime_of_mem_factorization Nat.prime_of_mem_factorization
+#noalign nat.support_factorization
 
-theorem pos_of_mem_factorization {n p : ℕ} (hp : p ∈ n.factorization.support) : 0 < p :=
-  Prime.pos (prime_of_mem_factorization hp)
-#align nat.pos_of_mem_factorization Nat.pos_of_mem_factorization
-
-theorem le_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) : p ≤ n :=
-  le_of_mem_factors (factor_iff_mem_factorization.mp h)
-#align nat.le_of_mem_factorization Nat.le_of_mem_factorization
+#align nat.factor_iff_mem_factorization Nat.mem_primeFactors_iff_mem_factors
+#align nat.prime_of_mem_factorization Nat.prime_of_mem_primeFactors
+#align nat.pos_of_mem_factorization Nat.pos_of_mem_primeFactors
+#align nat.le_of_mem_factorization Nat.le_of_mem_primeFactors
 
 /-! ## Lemmas characterising when `n.factorization p = 0` -/
 
 
 theorem factorization_eq_zero_iff (n p : ℕ) :
     n.factorization p = 0 ↔ ¬p.Prime ∨ ¬p ∣ n ∨ n = 0 := by
-  rw [← not_mem_support_iff, support_factorization, mem_toFinset]
-  rcases eq_or_ne n 0 with (rfl | hn)
-  · simp
-  · simp [hn, Nat.mem_factors, not_and_or, -not_and]
+  simp_rw [← not_mem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]
 #align nat.factorization_eq_zero_iff Nat.factorization_eq_zero_iff
 
 @[simp]
@@ -165,7 +183,7 @@ theorem factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) : n.factori
 #align nat.factorization_eq_zero_of_not_dvd Nat.factorization_eq_zero_of_not_dvd
 
 theorem factorization_eq_zero_of_lt {n p : ℕ} (h : n < p) : n.factorization p = 0 :=
-  Finsupp.not_mem_support_iff.mp (mt le_of_mem_factorization (not_le_of_lt h))
+  Finsupp.not_mem_support_iff.mp (mt le_of_mem_primeFactors (not_le_of_lt h))
 #align nat.factorization_eq_zero_of_lt Nat.factorization_eq_zero_of_lt
 
 @[simp]
@@ -179,7 +197,7 @@ theorem factorization_one_right (n : ℕ) : n.factorization 1 = 0 :=
 #align nat.factorization_one_right Nat.factorization_one_right
 
 theorem dvd_of_factorization_pos {n p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n :=
-  dvd_of_mem_factors (factor_iff_mem_factorization.1 (mem_support_iff.2 hn))
+  dvd_of_mem_factors $ mem_primeFactors_iff_mem_factors.1 $ mem_support_iff.2 hn
 #align nat.dvd_of_factorization_pos Nat.dvd_of_factorization_pos
 
 theorem Prime.factorization_pos_of_dvd {n p : ℕ} (hp : p.Prime) (hn : n ≠ 0) (h : p ∣ n) :
@@ -222,20 +240,13 @@ theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
     count_append]
 #align nat.factorization_mul Nat.factorization_mul
 
-theorem factorization_mul_support {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
-    (a * b).factorization.support = a.factorization.support ∪ b.factorization.support := by
-  ext q
-  simp only [Finset.mem_union, factor_iff_mem_factorization]
-  exact mem_factors_mul ha hb
-#align nat.factorization_mul_support Nat.factorization_mul_support
+#align nat.factorization_mul_support Nat.primeFactors_mul
 
 /-- If a product over `n.factorization` doesn't use the multiplicities of the prime factors
-then it's equal to the corresponding product over `n.factors.toFinset` -/
-theorem prod_factorization_eq_prod_factors {n : ℕ} {β : Type*} [CommMonoid β] (f : ℕ → β) :
-    (n.factorization.prod fun p _ => f p) = ∏ p in n.factors.toFinset, f p := by
-  apply prod_congr support_factorization
-  simp
-#align nat.prod_factorization_eq_prod_factors Nat.prod_factorization_eq_prod_factors
+then it's equal to the corresponding product over `n.primeFactors` -/
+theorem prod_factorization_eq_prod_primeFactors {β : Type*} [CommMonoid β] (f : ℕ → β) :
+    (n.factorization.prod fun p _ => f p) = ∏ p in n.primeFactors, f p := rfl
+#align nat.prod_factorization_eq_prod_factors Nat.prod_factorization_eq_prod_primeFactors
 
 /-- For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : Finset α`,
 the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`.
@@ -319,7 +330,7 @@ theorem eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf :
 
 /-- The equiv between `ℕ+` and `ℕ →₀ ℕ` with support in the primes. -/
 def factorizationEquiv : ℕ+ ≃ { f : ℕ →₀ ℕ | ∀ p ∈ f.support, Prime p } where
-  toFun := fun ⟨n, _⟩ => ⟨n.factorization, fun _ => prime_of_mem_factorization⟩
+  toFun := fun ⟨n, _⟩ => ⟨n.factorization, fun _ => prime_of_mem_primeFactors⟩
   invFun := fun ⟨f, hf⟩ =>
     ⟨f.prod _, prod_pow_pos_of_zero_not_mem_support fun H => not_prime_zero (hf 0 H)⟩
   left_inv := fun ⟨_, hx⟩ => Subtype.ext <| factorization_prod_pow_eq_self hx.ne.symm
@@ -415,12 +426,7 @@ theorem ord_compl_mul (a b p : ℕ) : ord_compl[p] (a * b) = ord_compl[p] a * or
 
 /-! ### Factorization and divisibility -/
 
-
-theorem dvd_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) : p ∣ n := by
-  rcases eq_or_ne n 0 with (rfl | hn)
-  · simp
-  simp [← mem_factors_iff_dvd hn (prime_of_mem_factorization h), factor_iff_mem_factorization.mp h]
-#align nat.dvd_of_mem_factorization Nat.dvd_of_mem_factorization
+#align nat.dvd_of_mem_factorization Nat.dvd_of_mem_primeFactors
 
 /-- A crude upper bound on `n.factorization p` -/
 theorem factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n := by
@@ -538,9 +544,7 @@ theorem factorization_ord_compl (n p : ℕ) :
   by_cases pp : p.Prime
   case neg =>
     -- porting note: needed to solve side goal explicitly
-    rw [Finsupp.erase_of_not_mem_support]
-    · simp [pp]
-    · simp [mt prime_of_mem_factors pp]
+    rw [Finsupp.erase_of_not_mem_support] <;> simp [pp]
   ext q
   rcases eq_or_ne q p with (rfl | hqp)
   · simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ord_compl pp hn]
@@ -651,12 +655,12 @@ theorem dvd_iff_prime_pow_dvd_dvd (n d : ℕ) :
   exact h p _ pp (ord_proj_dvd _ _)
 #align nat.dvd_iff_prime_pow_dvd_dvd Nat.dvd_iff_prime_pow_dvd_dvd
 
-theorem prod_prime_factors_dvd (n : ℕ) : (∏ p : ℕ in n.factors.toFinset, p) ∣ n := by
+theorem prod_primeFactors_dvd (n : ℕ) : ∏ p in n.primeFactors, p ∣ n := by
   by_cases hn : n = 0
   · subst hn
     simp
   simpa [prod_factors hn] using Multiset.toFinset_prod_dvd_prod (n.factors : Multiset ℕ)
-#align nat.prod_prime_factors_dvd Nat.prod_prime_factors_dvd
+#align nat.prod_prime_factors_dvd Nat.prod_primeFactors_dvd
 
 theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
     (gcd a b).factorization = a.factorization ⊓ b.factorization := by
@@ -692,20 +696,18 @@ theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
   exact (min_add_max _ _).symm
 #align nat.factorization_lcm Nat.factorization_lcm
 
-@[to_additive sum_factors_gcd_add_sum_factors_mul]
-theorem prod_factors_gcd_mul_prod_factors_mul {β : Type*} [CommMonoid β] (m n : ℕ) (f : ℕ → β) :
-    (m.gcd n).factors.toFinset.prod f * (m * n).factors.toFinset.prod f =
-      m.factors.toFinset.prod f * n.factors.toFinset.prod f := by
-  rcases eq_or_ne n 0 with (rfl | hm0)
+@[to_additive sum_primeFactors_gcd_add_sum_primeFactors_mul]
+theorem prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type*} [CommMonoid β] (m n : ℕ)
+    (f : ℕ → β) :
+    (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f =
+      m.primeFactors.prod f * n.primeFactors.prod f := by
+  obtain rfl | hm₀ := eq_or_ne m 0
   · simp
-  rcases eq_or_ne m 0 with (rfl | hn0)
+  obtain rfl | hn₀ := eq_or_ne n 0
   · simp
-  rw [← @Finset.prod_union_inter _ _ m.factors.toFinset n.factors.toFinset, mul_comm]
-  congr
-  · apply factors_mul_toFinset <;> assumption
-  · simp only [← support_factorization, factorization_gcd hn0 hm0, Finsupp.support_inf]
-#align nat.prod_factors_gcd_mul_prod_factors_mul Nat.prod_factors_gcd_mul_prod_factors_mul
-#align nat.sum_factors_gcd_add_sum_factors_mul Nat.sum_factors_gcd_add_sum_factors_mul
+  · rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
+#align nat.prod_factors_gcd_mul_prod_factors_mul Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul
+#align nat.sum_factors_gcd_add_sum_factors_mul Nat.sum_primeFactors_gcd_add_sum_primeFactors_mul
 
 theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
     { i : ℕ | i ≠ 0 ∧ p ^ i ∣ n } = Set.Icc 1 (n.factorization p) := by
@@ -911,16 +913,14 @@ theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n <
     rw [← factorization_prod_pow_eq_self hn]
   rw [eq_comm]
   apply Finset.prod_subset_one_on_sdiff
-  · exact fun p hp =>
-      Finset.mem_filter.mpr
-        ⟨Finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
-          prime_of_mem_factorization hp⟩
+  · exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
+      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩
   · intro p hp
     cases' Finset.mem_sdiff.mp hp with hp1 hp2
     rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
     simp [Finsupp.not_mem_support_iff.mp hp2]
   · intro p hp
-    simp [factorization_def n (prime_of_mem_factorization hp)]
+    simp [factorization_def n (prime_of_mem_primeFactors hp)]
 #align nat.prod_pow_prime_padic_val_nat Nat.prod_pow_prime_padicValNat
 
 /-! ### Lemmas about factorizations of particular functions -/
diff --git a/Mathlib/Data/Nat/Factorization/PrimePow.lean b/Mathlib/Data/Nat/Factorization/PrimePow.lean
index 542eef569f8f0..c1fc8a1420f26 100644
--- a/Mathlib/Data/Nat/Factorization/PrimePow.lean
+++ b/Mathlib/Data/Nat/Factorization/PrimePow.lean
@@ -29,9 +29,8 @@ theorem isPrimePow_of_minFac_pow_factorization_eq {n : ℕ}
   rcases eq_or_ne n 0 with (rfl | hn')
   · simp_all
   refine' ⟨_, _, (Nat.minFac_prime hn).prime, _, h⟩
-  rw [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.factor_iff_mem_factorization,
-    Nat.mem_factors_iff_dvd hn' (Nat.minFac_prime hn)]
-  apply Nat.minFac_dvd
+  simp [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.support_factorization, hn',
+    Nat.minFac_prime hn, Nat.minFac_dvd]
 #align is_prime_pow_of_min_fac_pow_factorization_eq isPrimePow_of_minFac_pow_factorization_eq
 
 theorem isPrimePow_iff_minFac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) :
@@ -51,8 +50,8 @@ theorem isPrimePow_iff_factorization_eq_single {n : ℕ} :
       rintro rfl
       simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
     rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
-    exact
-      ⟨Nat.prime_of_mem_factorization (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩
+    exact ⟨Nat.prime_of_mem_primeFactors $
+      Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩
 #align is_prime_pow_iff_factorization_eq_single isPrimePow_iff_factorization_eq_single
 
 theorem isPrimePow_iff_card_support_factorization_eq_one {n : ℕ} :
diff --git a/Mathlib/Data/Nat/Factors.lean b/Mathlib/Data/Nat/Factors.lean
index d1f0a790bb47a..81acf4a51e590 100644
--- a/Mathlib/Data/Nat/Factors.lean
+++ b/Mathlib/Data/Nat/Factors.lean
@@ -154,6 +154,9 @@ theorem mem_factors {n p} (hn : n ≠ 0) : p ∈ factors n ↔ Prime p ∧ p ∣
     (mem_factors_iff_dvd hn hprime).mpr hdvd⟩
 #align nat.mem_factors Nat.mem_factors
 
+@[simp] lemma mem_factors' {n p} : p ∈ n.factors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
+  cases n <;> simp [mem_factors, *]
+
 theorem le_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) : p ≤ n := by
   rcases n.eq_zero_or_pos with (rfl | hn)
   · rw [factors_zero] at h
diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean
index e04564b3a3b11..9d202c8b65ae8 100644
--- a/Mathlib/Data/Nat/Totient.lean
+++ b/Mathlib/Data/Nat/Totient.lean
@@ -286,40 +286,40 @@ theorem totient_eq_prod_factorization {n : ℕ} (hn : n ≠ 0) :
   apply Finsupp.prod_congr _
   intro p hp
   have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
-  rw [totient_prime_pow (prime_of_mem_factorization hp) h]
+  rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]
 #align nat.totient_eq_prod_factorization Nat.totient_eq_prod_factorization
 
 /-- Euler's product formula for the totient function. -/
-theorem totient_mul_prod_factors (n : ℕ) :
-    (φ n * ∏ p in n.factors.toFinset, p) = n * ∏ p in n.factors.toFinset, (p - 1) := by
+theorem totient_mul_prod_primeFactors (n : ℕ) :
+    (φ n * ∏ p in n.primeFactors, p) = n * ∏ p in n.primeFactors, (p - 1) := by
   by_cases hn : n = 0; · simp [hn]
   rw [totient_eq_prod_factorization hn]
   nth_rw 3 [← factorization_prod_pow_eq_self hn]
-  simp only [← prod_factorization_eq_prod_factors, ← Finsupp.prod_mul]
+  simp only [← prod_factorization_eq_prod_primeFactors, ← Finsupp.prod_mul]
   refine' Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => _
   rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
   rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
-#align nat.totient_mul_prod_factors Nat.totient_mul_prod_factors
+#align nat.totient_mul_prod_factors Nat.totient_mul_prod_primeFactors
 
 /-- Euler's product formula for the totient function. -/
-theorem totient_eq_div_factors_mul (n : ℕ) :
-    φ n = (n / ∏ p in n.factors.toFinset, p) * ∏ p in n.factors.toFinset, (p - 1) := by
-  rw [← mul_div_left n.totient, totient_mul_prod_factors, mul_comm,
-    Nat.mul_div_assoc _ (prod_prime_factors_dvd n), mul_comm]
-  have := prod_pos (fun p => pos_of_mem_factorization (n := n))
-  simpa [prod_factorization_eq_prod_factors] using this
-#align nat.totient_eq_div_factors_mul Nat.totient_eq_div_factors_mul
+theorem totient_eq_div_primeFactors_mul (n : ℕ) :
+    φ n = (n / ∏ p in n.primeFactors, p) * ∏ p in n.primeFactors, (p - 1) := by
+  rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
+    Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]
+  have := prod_pos (fun p => pos_of_mem_primeFactors (n := n))
+  simpa [prod_factorization_eq_prod_primeFactors] using this
+#align nat.totient_eq_div_factors_mul Nat.totient_eq_div_primeFactors_mul
 
 /-- Euler's product formula for the totient function. -/
 theorem totient_eq_mul_prod_factors (n : ℕ) :
-    (φ n : ℚ) = n * ∏ p in n.factors.toFinset, (1 - (p : ℚ)⁻¹) := by
+    (φ n : ℚ) = n * ∏ p in n.primeFactors, (1 - (p : ℚ)⁻¹) := by
   by_cases hn : n = 0
   · simp [hn]
   have hn' : (n : ℚ) ≠ 0 := by simp [hn]
-  have hpQ : (∏ p in n.factors.toFinset, (p : ℚ)) ≠ 0 := by
-    rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
-    exact prod_pos fun p hp => pos_of_mem_factorization hp
-  simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod,
+  have hpQ : (∏ p in n.primeFactors, (p : ℚ)) ≠ 0 := by
+    rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_primeFactors]
+    exact prod_pos fun p hp => pos_of_mem_primeFactors hp
+  simp only [totient_eq_div_primeFactors_mul n, prod_primeFactors_dvd n, cast_mul, cast_prod,
     cast_div_charZero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]
   refine' prod_congr rfl fun p hp => _
   have hp := pos_of_mem_factors (List.mem_toFinset.mp hp)
@@ -337,13 +337,13 @@ theorem totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ
       _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
         congr 1
         exact div_mul_div_comm h1 h2
-  simp only [totient_eq_div_factors_mul]
+  simp only [totient_eq_div_primeFactors_mul]
   rw [shuffle, shuffle]
   rotate_left
-  repeat' apply prod_prime_factors_dvd
-  · simp only [prod_factors_gcd_mul_prod_factors_mul]
+  repeat' apply prod_primeFactors_dvd
+  · simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]
     rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
-    exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b)
+    exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)
 #align nat.totient_gcd_mul_totient_mul Nat.totient_gcd_mul_totient_mul
 
 theorem totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) := by
@@ -361,10 +361,7 @@ theorem totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : φ a ∣ φ b := by
   · simp [zero_dvd_iff.1 h]
   rcases eq_or_ne b 0 with (rfl | hb0)
   · simp
-  have hab' : a.factorization.support ⊆ b.factorization.support := by
-    intro p
-    simp only [support_factorization, List.mem_toFinset]
-    apply factors_subset_of_dvd h hb0
+  have hab' := primeFactors_mono h hb0
   rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
   refine' Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul _ dvd_rfl
   exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)
diff --git a/Mathlib/NumberTheory/MaricaSchoenheim.lean b/Mathlib/NumberTheory/MaricaSchoenheim.lean
new file mode 100644
index 0000000000000..68841fdb79ed9
--- /dev/null
+++ b/Mathlib/NumberTheory/MaricaSchoenheim.lean
@@ -0,0 +1,39 @@
+import Mathlib.Combinatorics.SetFamily.FourFunctions
+import Mathlib.Data.Nat.Squarefree
+
+open Finset
+open scoped BigOperators FinsetFamily
+
+namespace Nat
+
+/-- A special case of Graham's conjecture. -/
+lemma marica_schoenheim {n : ℕ} (f : ℕ → ℕ) (hn : n ≠ 0) (hf : StrictMonoOn f (Set.Iio n))
+    (hf' : ∀ k < n, Squarefree (f k)) : ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i := by
+  by_contra'
+  set 𝒜 := (Iio n).image fun n ↦ primeFactors (f n)
+  have hf'' : ∀ i < n, ∀ j, Squarefree (f i / (f i).gcd (f j)) :=
+    fun i hi j ↦ (hf' _ hi).squarefree_of_dvd $ div_dvd_of_dvd $ gcd_dvd_left _ _
+  refine lt_irrefl n ?_
+  calc
+    n = 𝒜.card := ?_
+    _ ≤ (𝒜 \\ 𝒜).card := 𝒜.card_le_card_diffs
+    _ ≤ (Ioo 0 n).card := card_le_card_of_inj_on (fun s ↦ ∏ p in s, p) ?_ ?_
+    _ = n - 1 := by rw [card_Ioo, tsub_zero]
+    _ < n := tsub_lt_self hn.bot_lt zero_lt_one
+  · rw [card_image_of_injOn, card_Iio]
+    simpa using prod_primeFactors_invOn_squarefree.2.injOn.comp hf.injOn hf'
+  · simp only [forall_mem_diffs, forall_image, mem_Ioo, mem_Iio]
+    rintro i hi j hj
+    rw [←primeFactors_div_gcd (hf' _ hi) (hf' _ hj).ne_zero,
+      prod_primeFactors_of_squarefree $ hf'' _ hi _]
+    exact ⟨Nat.div_pos (gcd_le_left _ (hf' _ hi).ne_zero.bot_lt) $
+      Nat.gcd_pos_of_pos_left _ (hf' _ hi).ne_zero.bot_lt, Nat.div_lt_of_lt_mul $ this _ hi _ hj⟩
+  · simp only [forall_mem_diffs, forall_image, mem_Ioo, mem_Iio]
+    rintro a ha b hb c hc d hd
+    rw [←primeFactors_div_gcd (hf' _ ha) (hf' _ hb).ne_zero, ←primeFactors_div_gcd
+      (hf' _ hc) (hf' _ hd).ne_zero, prod_primeFactors_of_squarefree (hf'' _ ha _),
+      prod_primeFactors_of_squarefree (hf'' _ hc _)]
+    rintro h
+    rw [h]
+
+end Nat

From 8f1eb490f8b90b30303dcbef68f94c513d9994d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 3 Nov 2023 22:26:24 +0000
Subject: [PATCH 2/6] fix NumberTheory.ArithmeticFunction

---
 Mathlib/NumberTheory/ArithmeticFunction.lean |  5 +--
 Mathlib/NumberTheory/MaricaSchoenheim.lean   | 39 --------------------
 2 files changed, 1 insertion(+), 43 deletions(-)
 delete mode 100644 Mathlib/NumberTheory/MaricaSchoenheim.lean

diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
index 2b8869c045d5f..2b282e395fadb 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -751,10 +751,7 @@ theorem eq_iff_eq_on_prime_powers [CommMonoidWithZero R] (f : ArithmeticFunction
   by_cases hn : n = 0
   · rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
   rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]
-  refine' Finset.prod_congr rfl _
-  simp only [support_factorization, List.mem_toFinset]
-  intro p hp
-  exact h p _ (Nat.prime_of_mem_factors hp)
+  exact Finset.prod_congr rfl fun p hp ↦ h p _ (Nat.prime_of_mem_primeFactors hp)
 #align nat.arithmetic_function.is_multiplicative.eq_iff_eq_on_prime_powers Nat.ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers
 
 theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R}
diff --git a/Mathlib/NumberTheory/MaricaSchoenheim.lean b/Mathlib/NumberTheory/MaricaSchoenheim.lean
deleted file mode 100644
index 68841fdb79ed9..0000000000000
--- a/Mathlib/NumberTheory/MaricaSchoenheim.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import Mathlib.Combinatorics.SetFamily.FourFunctions
-import Mathlib.Data.Nat.Squarefree
-
-open Finset
-open scoped BigOperators FinsetFamily
-
-namespace Nat
-
-/-- A special case of Graham's conjecture. -/
-lemma marica_schoenheim {n : ℕ} (f : ℕ → ℕ) (hn : n ≠ 0) (hf : StrictMonoOn f (Set.Iio n))
-    (hf' : ∀ k < n, Squarefree (f k)) : ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i := by
-  by_contra'
-  set 𝒜 := (Iio n).image fun n ↦ primeFactors (f n)
-  have hf'' : ∀ i < n, ∀ j, Squarefree (f i / (f i).gcd (f j)) :=
-    fun i hi j ↦ (hf' _ hi).squarefree_of_dvd $ div_dvd_of_dvd $ gcd_dvd_left _ _
-  refine lt_irrefl n ?_
-  calc
-    n = 𝒜.card := ?_
-    _ ≤ (𝒜 \\ 𝒜).card := 𝒜.card_le_card_diffs
-    _ ≤ (Ioo 0 n).card := card_le_card_of_inj_on (fun s ↦ ∏ p in s, p) ?_ ?_
-    _ = n - 1 := by rw [card_Ioo, tsub_zero]
-    _ < n := tsub_lt_self hn.bot_lt zero_lt_one
-  · rw [card_image_of_injOn, card_Iio]
-    simpa using prod_primeFactors_invOn_squarefree.2.injOn.comp hf.injOn hf'
-  · simp only [forall_mem_diffs, forall_image, mem_Ioo, mem_Iio]
-    rintro i hi j hj
-    rw [←primeFactors_div_gcd (hf' _ hi) (hf' _ hj).ne_zero,
-      prod_primeFactors_of_squarefree $ hf'' _ hi _]
-    exact ⟨Nat.div_pos (gcd_le_left _ (hf' _ hi).ne_zero.bot_lt) $
-      Nat.gcd_pos_of_pos_left _ (hf' _ hi).ne_zero.bot_lt, Nat.div_lt_of_lt_mul $ this _ hi _ hj⟩
-  · simp only [forall_mem_diffs, forall_image, mem_Ioo, mem_Iio]
-    rintro a ha b hb c hc d hd
-    rw [←primeFactors_div_gcd (hf' _ ha) (hf' _ hb).ne_zero, ←primeFactors_div_gcd
-      (hf' _ hc) (hf' _ hd).ne_zero, prod_primeFactors_of_squarefree (hf'' _ ha _),
-      prod_primeFactors_of_squarefree (hf'' _ hc _)]
-    rintro h
-    rw [h]
-
-end Nat

From f29464f40096c2e9502bdf2aecb767ac4cd9b712 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 3 Nov 2023 23:47:54 +0000
Subject: [PATCH 3/6] move to PrimeFin

---
 Mathlib/Data/Nat/Factorization/Basic.lean     | 39 ---------
 Mathlib/Data/Nat/PrimeFin.lean                | 79 +++++++++++++------
 Mathlib/GroupTheory/Exponent.lean             |  2 +-
 Mathlib/GroupTheory/Sylow.lean                | 12 +--
 .../Cyclotomic/PrimitiveRoots.lean            |  2 +-
 5 files changed, 65 insertions(+), 69 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
index 2eeb4972575a3..034b31d8f2463 100644
--- a/Mathlib/Data/Nat/Factorization/Basic.lean
+++ b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -49,45 +49,6 @@ open BigOperators
 namespace Nat
 variable {a b m n p : ℕ}
 
-/-- The prime factors of a natural number as a finset. -/
-@[pp_dot] def primeFactors (n : ℕ) : Finset ℕ := n.factors.toFinset
-
-@[simp] lemma toFinset_factors (n : ℕ) : n.factors.toFinset = n.primeFactors := rfl
-
-@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
-  simp_rw [←toFinset_factors, List.mem_toFinset, mem_factors']
-
-lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by
-  simp [hn]
-
-lemma primeFactors_mono (hmn : m ∣ n) (hn : n ≠ 0) : primeFactors m ⊆ primeFactors n := by
-  simp only [subset_iff, mem_primeFactors, and_imp]
-  exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩
-
-lemma mem_primeFactors_iff_mem_factors : p ∈ n.primeFactors ↔ p ∈ n.factors := by
-  simp only [primeFactors, List.mem_toFinset]
-
-lemma prime_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p.Prime := (mem_primeFactors.1 hp).1
-lemma dvd_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p ∣ n := (mem_primeFactors.1 hp).2.1
-
-lemma pos_of_mem_primeFactors (hp : p ∈ n.primeFactors) : 0 < p :=
-  (prime_of_mem_primeFactors hp).pos
-
-lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
-  le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt $ dvd_of_mem_primeFactors h
-
-@[simp] lemma primeFactors_zero : primeFactors 0 = ∅ := rfl
-@[simp] lemma primeFactors_one : primeFactors 0 = ∅ := rfl
-
-lemma primeFactors_mul (ha : a ≠ 0) (hb : b ≠ 0) :
-    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors := by
-  ext
-  simp only [Finset.mem_union, mem_primeFactors_iff_mem_factors, mem_factors_mul ha hb]
-
-lemma primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) :
-    (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors := by
-  ext; simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]; aesop
-
 /-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
  mapping each prime factor of `n` to its multiplicity in `n`. -/
 def factorization (n : ℕ) : ℕ →₀ ℕ where
diff --git a/Mathlib/Data/Nat/PrimeFin.lean b/Mathlib/Data/Nat/PrimeFin.lean
index f1874bd20c685..326eddcfd484b 100644
--- a/Mathlib/Data/Nat/PrimeFin.lean
+++ b/Mathlib/Data/Nat/PrimeFin.lean
@@ -15,8 +15,10 @@ import Mathlib.Data.Set.Finite
 This file contains some results about prime numbers which depend on finiteness of sets.
 -/
 
+open Finset
 
 namespace Nat
+variable {a b k m n p : ℕ}
 
 /-- A version of `Nat.exists_infinite_primes` using the `Set.Infinite` predicate. -/
 theorem infinite_setOf_prime : { p | Prime p }.Infinite :=
@@ -27,37 +29,70 @@ instance Primes.infinite : Infinite Primes := infinite_setOf_prime.to_subtype
 
 instance Primes.countable : Countable Primes := ⟨⟨coeNat.coe, coe_nat_injective⟩⟩
 
-/-- If `a`, `b` are positive, the prime divisors of `a * b` are the union of those of `a` and `b` -/
-theorem factors_mul_toFinset {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
-    (a * b).factors.toFinset = a.factors.toFinset ∪ b.factors.toFinset :=
-  (List.toFinset.ext fun _ => (mem_factors_mul ha hb).trans List.mem_union_iff.symm).trans <|
-    List.toFinset_union _ _
-#align nat.factors_mul_to_finset Nat.factors_mul_toFinset
+/-- The prime factors of a natural number as a finset. -/
+@[pp_dot] def primeFactors (n : ℕ) : Finset ℕ := n.factors.toFinset
 
-theorem pow_succ_factors_toFinset (n k : ℕ) :
-    (n ^ (k + 1)).factors.toFinset = n.factors.toFinset := by
+@[simp] lemma toFinset_factors (n : ℕ) : n.factors.toFinset = n.primeFactors := rfl
+
+@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
+  simp_rw [←toFinset_factors, List.mem_toFinset, mem_factors']
+
+lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by
+  simp [hn]
+
+lemma primeFactors_mono (hmn : m ∣ n) (hn : n ≠ 0) : primeFactors m ⊆ primeFactors n := by
+  simp only [subset_iff, mem_primeFactors, and_imp]
+  exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩
+
+lemma mem_primeFactors_iff_mem_factors : p ∈ n.primeFactors ↔ p ∈ n.factors := by
+  simp only [primeFactors, List.mem_toFinset]
+
+lemma prime_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p.Prime := (mem_primeFactors.1 hp).1
+lemma dvd_of_mem_primeFactors (hp : p ∈ n.primeFactors) : p ∣ n := (mem_primeFactors.1 hp).2.1
+
+lemma pos_of_mem_primeFactors (hp : p ∈ n.primeFactors) : 0 < p :=
+  (prime_of_mem_primeFactors hp).pos
+
+lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
+  le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt $ dvd_of_mem_primeFactors h
+
+@[simp] lemma primeFactors_zero : primeFactors 0 = ∅ := rfl
+@[simp] lemma primeFactors_one : primeFactors 0 = ∅ := rfl
+
+@[simp] protected lemma Prime.primeFactors (hp : p.Prime) : p.primeFactors = {p} := by
+  simp [Nat.primeFactors, factors_prime hp]
+
+lemma primeFactors_mul (ha : a ≠ 0) (hb : b ≠ 0) :
+    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors := by
+  ext; simp only [Finset.mem_union, mem_primeFactors_iff_mem_factors, mem_factors_mul ha hb]
+#align nat.factors_mul_to_finset Nat.primeFactors_mul
+
+lemma Coprime.primeFactors_mul {a b : ℕ} (hab : Coprime a b) :
+    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors :=
+  (List.toFinset.ext <| mem_factors_mul_of_coprime hab).trans <| List.toFinset_union _ _
+#align nat.factors_mul_to_finset_of_coprime Nat.Coprime.primeFactors_mul
+
+lemma primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) :
+    (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors := by
+  ext; simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]; aesop
+
+lemma primeFactors_pow_succ (n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors := by
   rcases eq_or_ne n 0 with (rfl | hn)
   · simp
   induction' k with k ih
   · simp
-  · rw [pow_succ', factors_mul_toFinset hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
-#align nat.pow_succ_factors_to_finset Nat.pow_succ_factors_toFinset
+  · rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]
+#align nat.pow_succ_factors_to_finset Nat.primeFactors_pow_succ
 
-theorem pow_factors_toFinset (n : ℕ) {k : ℕ} (hk : k ≠ 0) :
-    (n ^ k).factors.toFinset = n.factors.toFinset := by
+lemma primeFactors_pow (n : ℕ) (hk : k ≠ 0) : (n ^ k).primeFactors = n.primeFactors := by
   cases k
   · simp at hk
-  rw [pow_succ_factors_toFinset]
-#align nat.pow_factors_to_finset Nat.pow_factors_toFinset
+  rw [primeFactors_pow_succ]
+#align nat.pow_factors_to_finset Nat.primeFactors_pow
 
 /-- The only prime divisor of positive prime power `p^k` is `p` itself -/
-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) :
-    (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
+lemma primeFactors_prime_pow (hk : k ≠ 0) (hp : Prime p) :
+    (p ^ k).primeFactors = {p} := by simp [primeFactors_pow p hk, hp]
+#align nat.prime_pow_prime_divisor Nat.primeFactors_prime_pow
 
 end Nat
diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean
index afcb06c881f5a..3bdd83a6b8595 100644
--- a/Mathlib/GroupTheory/Exponent.lean
+++ b/Mathlib/GroupTheory/Exponent.lean
@@ -209,7 +209,7 @@ theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ}
     exact fun hd =>
       hp.one_lt.not_le
         ((mul_le_iff_le_one_left he).mp <|
-          Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_factorization h) hd)
+          Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_primeFactors h) hd)
   obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ord_proj_dvd _ _
   obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
   refine' ⟨g ^ k, _⟩
diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
index 0b32be6cc8f3f..33fd273715f05 100644
--- a/Mathlib/GroupTheory/Sylow.lean
+++ b/Mathlib/GroupTheory/Sylow.lean
@@ -784,8 +784,8 @@ noncomputable def directProductOfNormal [Fintype G]
   let P : ∀ p, Sylow p G := default
   have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y := by
     rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
-    haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
-    haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
+    haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
+    haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
     have hne' : p₁ ≠ p₂ := by simpa using hne
     apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
     apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
@@ -795,7 +795,7 @@ noncomputable def directProductOfNormal [Fintype G]
   · -- here we need to help the elaborator with an explicit instantiation
     apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _
     rintro ⟨p, hp⟩
-    haveI hp' := Fact.mk (Nat.prime_of_mem_factorization hp)
+    haveI hp' := Fact.mk (Nat.prime_of_mem_primeFactors hp)
     haveI := subsingleton_of_normal _ (hn (P p))
     change (∀ P : Sylow p G, P) ≃* P p
     exact MulEquiv.piSubsingleton _ _
@@ -807,8 +807,8 @@ noncomputable def directProductOfNormal [Fintype G]
   · apply Subgroup.injective_noncommPiCoprod_of_independent
     apply independent_of_coprime_order hcomm
     rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
-    haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁)
-    haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂)
+    haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
+    haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
     have hne' : p₁ ≠ p₂ := by simpa using hne
     apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
   show card (∀ p : ps, P p) = card G
@@ -816,7 +816,7 @@ noncomputable def directProductOfNormal [Fintype G]
       card (∀ p : ps, P p) = ∏ p : ps, card (P p) := Fintype.card_pi
       _ = ∏ p : ps, p.1 ^ (card G).factorization p.1 := by
         congr 1 with ⟨p, hp⟩
-        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_factorization hp⟩ (P p)
+        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)
       _ = ∏ p in ps, p ^ (card G).factorization p :=
         (Finset.prod_finset_coe (fun p => p ^ (card G).factorization p) _)
       _ = (card G).factorization.prod (· ^ ·) := rfl
diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
index d520899da0a0d..6e64e5c3096e6 100644
--- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
@@ -296,7 +296,7 @@ theorem sub_one_norm_isPrimePow (hn : IsPrimePow (n : ℕ)) [IsCyclotomicExtensi
   obtain ⟨k, hk⟩ : ∃ k, (n : ℕ).factorization (n : ℕ).minFac = k + 1 :=
     exists_eq_succ_of_ne_zero
       (((n : ℕ).factorization.mem_support_toFun (n : ℕ).minFac).1 <|
-        factor_iff_mem_factorization.2 <|
+        mem_primeFactors_iff_mem_factors.2 <|
           (mem_factors (IsPrimePow.ne_zero hn)).2 ⟨hprime.out, minFac_dvd _⟩)
   simp [hk, sub_one_norm_eq_eval_cyclotomic hζ this hirr]
 #align is_primitive_root.sub_one_norm_is_prime_pow IsPrimitiveRoot.sub_one_norm_isPrimePow

From 6345b1b9f444a88b6c391959980b3fd091aae946 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 4 Nov 2023 08:39:44 +0000
Subject: [PATCH 4/6] upstream more lemmas

---
 Mathlib/Data/Nat/Factorization/Basic.lean    | 40 +++++---------------
 Mathlib/Data/Nat/Factorization/PrimePow.lean | 12 +++---
 Mathlib/Data/Nat/PrimeFin.lean               | 17 +++++++++
 Mathlib/GroupTheory/Nilpotent.lean           |  8 ++--
 Mathlib/GroupTheory/Sylow.lean               |  4 +-
 Mathlib/NumberTheory/ArithmeticFunction.lean |  2 +-
 6 files changed, 40 insertions(+), 43 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
index 034b31d8f2463..cde30865551fe 100644
--- a/Mathlib/Data/Nat/Factorization/Basic.lean
+++ b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -203,10 +203,9 @@ theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
 
 #align nat.factorization_mul_support Nat.primeFactors_mul
 
-/-- If a product over `n.factorization` doesn't use the multiplicities of the prime factors
-then it's equal to the corresponding product over `n.primeFactors` -/
-theorem prod_factorization_eq_prod_primeFactors {β : Type*} [CommMonoid β] (f : ℕ → β) :
-    (n.factorization.prod fun p _ => f p) = ∏ p in n.primeFactors, f p := rfl
+/-- A product over `n.factorization` can be written as a product over `n.primeFactors`; -/
+lemma prod_factorization_eq_prod_primeFactors {β : Type*} [CommMonoid β] (f : ℕ → ℕ → β) :
+    n.factorization.prod f = ∏ p in n.primeFactors, f p (n.factorization p) := rfl
 #align nat.prod_factorization_eq_prod_factors Nat.prod_factorization_eq_prod_primeFactors
 
 /-- For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : Finset α`,
@@ -734,19 +733,8 @@ theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : Coprime a b) (hpb
   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) :
-    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) :
-    (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)
-#align nat.factorization_mul_support_of_coprime Nat.factorization_mul_support_of_coprime
+#align nat.factorization_disjoint_of_coprime Nat.Coprime.disjoint_primeFactors
+#align nat.factorization_mul_support_of_coprime Nat.primeFactors_mul
 
 /-! ### Induction principles involving factorizations -/
 
@@ -832,25 +820,17 @@ theorem multiplicative_factorization {β : Type*} [CommMonoid β] (f : ℕ → 
   · intro a b _ _ hab ha hb hab_pos
     rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
       factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
-    convert factorization_disjoint_of_coprime hab
+    exact hab.disjoint_primeFactors
 #align nat.multiplicative_factorization Nat.multiplicative_factorization
 
 /-- 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) :
-    ∀ {n : ℕ}, f n = n.factorization.prod fun p k => f (p ^ k) := by
-  apply Nat.recOnPosPrimePosCoprime
-  · rintro p k hp -
-    simp only [hp.factorization_pow]
-    rw [prod_single_index _]
-    simp [hf1]
-  · simp [hf0]
-  · rw [factorization_one, hf1]
-    simp
-  · intro a b _ _ hab ha hb
-    rw [h_mult a b hab, ha, hb, factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
-    exact factorization_disjoint_of_coprime hab
+    f n = n.factorization.prod fun p k => f (p ^ k) := by
+  obtain rfl | hn := eq_or_ne n 0
+  · simpa
+  · exact multiplicative_factorization _ h_mult hf1 hn
 #align nat.multiplicative_factorization' Nat.multiplicative_factorization'
 
 /-- Two positive naturals are equal if their prime padic valuations are equal -/
diff --git a/Mathlib/Data/Nat/Factorization/PrimePow.lean b/Mathlib/Data/Nat/Factorization/PrimePow.lean
index c1fc8a1420f26..1e0a789d4ef69 100644
--- a/Mathlib/Data/Nat/Factorization/PrimePow.lean
+++ b/Mathlib/Data/Nat/Factorization/PrimePow.lean
@@ -54,11 +54,11 @@ theorem isPrimePow_iff_factorization_eq_single {n : ℕ} :
       Finsupp.mem_support_iff.2 (by simp [hn, hk.ne'] : n.factorization p ≠ 0), hk, rfl⟩
 #align is_prime_pow_iff_factorization_eq_single isPrimePow_iff_factorization_eq_single
 
-theorem isPrimePow_iff_card_support_factorization_eq_one {n : ℕ} :
-    IsPrimePow n ↔ n.factorization.support.card = 1 := by
-  simp_rw [isPrimePow_iff_factorization_eq_single, Finsupp.card_support_eq_one', exists_prop,
-    pos_iff_ne_zero]
-#align is_prime_pow_iff_card_support_factorization_eq_one isPrimePow_iff_card_support_factorization_eq_one
+theorem isPrimePow_iff_card_primeFactors_eq_one {n : ℕ} :
+    IsPrimePow n ↔ n.primeFactors.card = 1 := by
+  simp_rw [isPrimePow_iff_factorization_eq_single, ←Nat.support_factorization,
+    Finsupp.card_support_eq_one', exists_prop, pos_iff_ne_zero]
+#align is_prime_pow_iff_card_support_factorization_eq_one isPrimePow_iff_card_primeFactors_eq_one
 
 theorem IsPrimePow.exists_ord_compl_eq_one {n : ℕ} (h : IsPrimePow n) :
     ∃ p : ℕ, p.Prime ∧ ord_compl[p] n = 1 := by
@@ -136,7 +136,7 @@ theorem Nat.Coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.Coprime a b) (hn
     rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ←
       Finset.mem_inter]
     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
+    simpa using hab.disjoint_primeFactors.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
 
diff --git a/Mathlib/Data/Nat/PrimeFin.lean b/Mathlib/Data/Nat/PrimeFin.lean
index 326eddcfd484b..4f0c13ab91f30 100644
--- a/Mathlib/Data/Nat/PrimeFin.lean
+++ b/Mathlib/Data/Nat/PrimeFin.lean
@@ -59,6 +59,14 @@ lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
 @[simp] lemma primeFactors_zero : primeFactors 0 = ∅ := rfl
 @[simp] lemma primeFactors_one : primeFactors 0 = ∅ := rfl
 
+@[simp] lemma primeFactors_eq_empty : n.primeFactors = ∅ ↔ n = 0 ∨ n = 1 := by
+  constructor
+  · contrapose!
+    rintro hn
+    obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
+    exact Nonempty.ne_empty $ ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
+  · rintro (rfl | rfl) <;> simp
+
 @[simp] protected lemma Prime.primeFactors (hp : p.Prime) : p.primeFactors = {p} := by
   simp [Nat.primeFactors, factors_prime hp]
 
@@ -76,6 +84,15 @@ lemma primeFactors_gcd (ha : a ≠ 0) (hb : b ≠ 0) :
     (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors := by
   ext; simp [dvd_gcd_iff, ha, hb, gcd_ne_zero_left ha]; aesop
 
+@[simp] lemma disjoint_primeFactors (ha : a ≠ 0) (hb : b ≠ 0) :
+    Disjoint a.primeFactors b.primeFactors ↔ Coprime a b := by
+  simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ←primeFactors_gcd, gcd_ne_zero_left,
+    ha, hb]
+
+protected lemma Coprime.disjoint_primeFactors (hab : Coprime a b) :
+    Disjoint a.primeFactors b.primeFactors :=
+  List.disjoint_toFinset_iff_disjoint.2 $ coprime_factors_disjoint hab
+
 lemma primeFactors_pow_succ (n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors := by
   rcases eq_or_ne n 0 with (rfl | hn)
   · simp
diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean
index bbfa744e9af2c..5d6182105dfef 100644
--- a/Mathlib/GroupTheory/Nilpotent.lean
+++ b/Mathlib/GroupTheory/Nilpotent.lean
@@ -875,13 +875,13 @@ variable [Fintype G]
 
 /-- If a finite group is the direct product of its Sylow groups, it is nilpotent -/
 theorem isNilpotent_of_product_of_sylow_group
-    (e : (∀ p : (Fintype.card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G) :
+    (e : (∀ p : (Fintype.card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G) :
     IsNilpotent G := by
   classical
-    let ps := (Fintype.card G).factorization.support
+    let ps := (Fintype.card G).primeFactors
     have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
       intro p P
-      haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
+      haveI : Fact (Nat.Prime ↑p) := Fact.mk $ Nat.prime_of_mem_primeFactors p.2
       exact P.isPGroup'.isNilpotent
     exact nilpotent_of_mulEquiv e
 #align is_nilpotent_of_product_of_sylow_group isNilpotent_of_product_of_sylow_group
@@ -894,7 +894,7 @@ theorem isNilpotent_of_finite_tFAE :
       [IsNilpotent G, NormalizerCondition G, ∀ H : Subgroup G, IsCoatom H → H.Normal,
         ∀ (p : ℕ) (_hp : Fact p.Prime) (P : Sylow p G), (↑P : Subgroup G).Normal,
         Nonempty
-          ((∀ p : (card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)] := by
+          ((∀ p : (card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)] := by
   tfae_have 1 → 2
   · exact @normalizerCondition_of_isNilpotent _ _
   tfae_have 2 → 3
diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
index 33fd273715f05..09e5975549082 100644
--- a/Mathlib/GroupTheory/Sylow.lean
+++ b/Mathlib/GroupTheory/Sylow.lean
@@ -778,8 +778,8 @@ of these Sylow subgroups.
 -/
 noncomputable def directProductOfNormal [Fintype G]
     (hn : ∀ {p : ℕ} [Fact p.Prime] (P : Sylow p G), (↑P : Subgroup G).Normal) :
-    (∀ p : (card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G := by
-  set ps := (Fintype.card G).factorization.support
+    (∀ p : (card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G := by
+  set ps := (Fintype.card G).primeFactors
   -- “The” Sylow subgroup for p
   let P : ∀ p, Sylow p G := default
   have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y := by
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
index 2b282e395fadb..8bb528aa840fa 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -767,7 +767,7 @@ theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R
   · intro i; rw [pow_zero, hf.1]
   iterate 4 rw [hf.multiplicative_factorization f (by assumption),
     Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
-      (s := (x.factorization.support ⊔ y.factorization.support))]
+      (s := (x.primeFactors ⊔ y.primeFactors))]
   · rw [←Finset.prod_mul_distrib, ←Finset.prod_mul_distrib]
     apply Finset.prod_congr rfl
     intro p _

From 56e47e66ea28902301724ee5d4d2a1841cf72389 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 4 Nov 2023 08:40:46 +0000
Subject: [PATCH 5/6] fix NumberTheory.ArithmeticFunction

---
 Mathlib/NumberTheory/ArithmeticFunction.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
index 8bb528aa840fa..ef887605ea30e 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -779,7 +779,7 @@ theorem lcm_apply_mul_gcd_apply [CommMonoidWithZero R] {f : ArithmeticFunction R
   · apply Finset.subset_union_left
   · rw [factorization_gcd hx hy, Finsupp.support_inf, Finset.sup_eq_union]
     apply Finset.inter_subset_union
-  · rw [factorization_lcm hx hy, Finsupp.support_sup, Finset.sup_eq_union]
+  · simp [factorization_lcm hx hy]
 
 end IsMultiplicative
 

From 379bade7f50d493fdf1099d2a12c3b7ef9b7cef3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 4 Nov 2023 10:34:45 +0000
Subject: [PATCH 6/6] fix Data.Nat.Totient

---
 Mathlib/Data/Nat/Factorization/Basic.lean | 4 ++++
 Mathlib/Data/Nat/Totient.lean             | 7 +++----
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean
index cde30865551fe..895b6a80f36b0 100644
--- a/Mathlib/Data/Nat/Factorization/Basic.lean
+++ b/Mathlib/Data/Nat/Factorization/Basic.lean
@@ -208,6 +208,10 @@ lemma prod_factorization_eq_prod_primeFactors {β : Type*} [CommMonoid β] (f :
     n.factorization.prod f = ∏ p in n.primeFactors, f p (n.factorization p) := rfl
 #align nat.prod_factorization_eq_prod_factors Nat.prod_factorization_eq_prod_primeFactors
 
+/-- A product over `n.primeFactors` can be written as a product over `n.factorization`; -/
+lemma prod_primeFactors_prod_factorization {β : Type*} [CommMonoid β] (f : ℕ → β) :
+    ∏ p in n.primeFactors, f p = n.factorization.prod (fun p _ ↦ f p) := rfl
+
 /-- For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : Finset α`,
 the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`.
 Generalises `factorization_mul`, which is the special case where `S.card = 2` and `g = id`. -/
diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean
index 9d202c8b65ae8..8cb21ef312555 100644
--- a/Mathlib/Data/Nat/Totient.lean
+++ b/Mathlib/Data/Nat/Totient.lean
@@ -295,7 +295,7 @@ theorem totient_mul_prod_primeFactors (n : ℕ) :
   by_cases hn : n = 0; · simp [hn]
   rw [totient_eq_prod_factorization hn]
   nth_rw 3 [← factorization_prod_pow_eq_self hn]
-  simp only [← prod_factorization_eq_prod_primeFactors, ← Finsupp.prod_mul]
+  simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]
   refine' Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => _
   rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
   rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
@@ -306,8 +306,7 @@ theorem totient_eq_div_primeFactors_mul (n : ℕ) :
     φ n = (n / ∏ p in n.primeFactors, p) * ∏ p in n.primeFactors, (p - 1) := by
   rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
     Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]
-  have := prod_pos (fun p => pos_of_mem_primeFactors (n := n))
-  simpa [prod_factorization_eq_prod_primeFactors] using this
+  exact prod_pos (fun p => pos_of_mem_primeFactors)
 #align nat.totient_eq_div_factors_mul Nat.totient_eq_div_primeFactors_mul
 
 /-- Euler's product formula for the totient function. -/
@@ -317,7 +316,7 @@ theorem totient_eq_mul_prod_factors (n : ℕ) :
   · simp [hn]
   have hn' : (n : ℚ) ≠ 0 := by simp [hn]
   have hpQ : (∏ p in n.primeFactors, (p : ℚ)) ≠ 0 := by
-    rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_primeFactors]
+    rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, prod_primeFactors_prod_factorization]
     exact prod_pos fun p hp => pos_of_mem_primeFactors hp
   simp only [totient_eq_div_primeFactors_mul n, prod_primeFactors_dvd n, cast_mul, cast_prod,
     cast_div_charZero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]