chore(Data): remove primes from names (#25163)

This PR renames lemmas that use a `'`, addressing technical debt. This focuses on declarations that seem simple to rename.



Co-authored-by: Bolton Bailey <bolton.bailey@gmail.com>

Author: BoltonBailey

Mathlib/Data/Finset/Functor.lean

@@ -116,7 +116,7 @@ instance lawfulApplicative : LawfulApplicative Finset :=
         exact hb
     pure_seq := fun f s => by simp only [pure_def, seq_def, sup_singleton, fmap_def]
     map_pure := fun _ _ => image_singleton _ _
-    seq_pure := fun _ _ => sup_singleton'' _ _
+    seq_pure := fun _ _ => sup_singleton_apply _ _
     seq_assoc := fun s t u => by
       ext a
       simp_rw [seq_def, fmap_def]
@@ -153,7 +153,7 @@ theorem bind_def {α β} : (· >>= ·) = sup (α := Finset α) (β := β) :=
 
 instance : LawfulMonad Finset :=
   { Finset.lawfulApplicative with
-    bind_pure_comp := fun _ _ => sup_singleton'' _ _
+    bind_pure_comp := fun _ _ => sup_singleton_apply _ _
     bind_map := fun _ _ => rfl
     pure_bind := fun _ _ => sup_singleton
     bind_assoc := fun s f g => by simp only [bind, ← sup_biUnion, sup_eq_biUnion, biUnion_biUnion] }

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -1132,14 +1132,20 @@ set_option linter.docPrime false in
   induction' s using cons_induction <;> simp [*]
 
 @[simp]
-theorem sup_singleton'' (s : Finset β) (f : β → α) :
+theorem sup_singleton_apply (s : Finset β) (f : β → α) :
     (s.sup fun b => {f b}) = s.image f := by
   ext a
   rw [mem_sup, mem_image]
   simp only [mem_singleton, eq_comm]
 
+@[deprecated (since := "2025-05-24")]
+alias sup_singleton'' := sup_singleton_apply
+
 @[simp]
-theorem sup_singleton' (s : Finset α) : s.sup singleton = s :=
-  (s.sup_singleton'' _).trans image_id
+theorem sup_singleton_eq_self (s : Finset α) : s.sup singleton = s :=
+  (s.sup_singleton_apply _).trans image_id
+
+@[deprecated (since := "2025-05-24")]
+alias sup_singleton' := sup_singleton_eq_self
 
 end Finset

Mathlib/Data/Int/Init.lean

@@ -310,13 +310,16 @@ lemma sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign
 @[simp] lemma toNat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.toNat - 1 : ℕ) : ℤ) = i - 1 := by
   simp only [lt_toNat, Int.cast_ofNat_Int, h, natCast_pred_of_pos, Int.le_of_lt h, toNat_of_nonneg]
 
-lemma toNat_lt'' {n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < n := by omega
+lemma toNat_lt_of_ne_zero {n : ℕ} (hn : n ≠ 0) : m.toNat < n ↔ m < n := by omega
+
+@[deprecated (since := "2025-05-24")]
+alias toNat_lt'' := toNat_lt_of_ne_zero
 
 /-- The modulus of an integer by another as a natural. Uses the E-rounding convention. -/
 def natMod (m n : ℤ) : ℕ := (m % n).toNat
 
 lemma natMod_lt {n : ℕ} (hn : n ≠ 0) : m.natMod n < n :=
-  (toNat_lt'' hn).2 <| emod_lt_of_pos _ <| by omega
+  (toNat_lt_of_ne_zero hn).2 <| emod_lt_of_pos _ <| by omega
 
 /-- For use in `Mathlib/Tactic/NormNum/Pow.lean` -/
 @[simp] lemma pow_eq (m : ℤ) (n : ℕ) : m.pow n = m ^ n := rfl

Mathlib/Data/Int/NatPrime.lean

@@ -18,7 +18,7 @@ namespace Int
 
 theorem not_prime_of_int_mul {a b : ℤ} {c : ℕ} (ha : a.natAbs ≠ 1) (hb : b.natAbs ≠ 1)
     (hc : a * b = (c : ℤ)) : ¬Nat.Prime c :=
-  not_prime_mul' (natAbs_mul_natAbs_eq hc) ha hb
+  not_prime_of_mul_eq (natAbs_mul_natAbs_eq hc) ha hb
 
 theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Nat.Prime p) {m n : ℤ}
     {k l : ℕ} (hpm : ↑(p ^ k) ∣ m) (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k + l + 1)) ∣ m * n) :

Mathlib/Data/Nat/ChineseRemainder.lean

@@ -39,7 +39,7 @@ lemma modEq_list_prod_iff {a b} {l : List ℕ} (co : l.Pairwise Coprime) :
       cases i using Fin.cases <;> simp_all
     · intro h; exact ⟨h 0, fun i => h i.succ⟩
 
-lemma modEq_list_prod_iff' {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairwise (Coprime on s)) :
+lemma modEq_list_map_prod_iff {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairwise (Coprime on s)) :
     a ≡ b [MOD (l.map s).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i] := by
   induction' l with i l ih
   · simp [modEq_one]
@@ -50,6 +50,9 @@ lemma modEq_list_prod_iff' {a b} {s : ι → ℕ} {l : List ι} (co : l.Pairwise
       exact (List.pairwise_cons.mp co).1 j hj
     simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]
 
+@[deprecated (since := "2025-05-24")]
+alias modEq_list_prod_iff' := modEq_list_map_prod_iff
+
 variable (a s : ι → ℕ)
 
 /-- The natural number less than `(l.map s).prod` congruent to
@@ -68,7 +71,7 @@ def chineseRemainderOfList : (l : List ι) → l.Pairwise (Coprime on s) →
     use k
     simp only [List.mem_cons, forall_eq_or_imp, k.prop.1, true_and]
     intro j hj
-    exact ((modEq_list_prod_iff' co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)
+    exact ((modEq_list_map_prod_iff co.of_cons).mp k.prop.2 j hj).trans (ih.prop j hj)
 
 @[simp] theorem chineseRemainderOfList_nil :
     (chineseRemainderOfList a s [] List.Pairwise.nil : ℕ) = 0 := rfl

Mathlib/Data/Nat/Pairing.lean

@@ -50,9 +50,12 @@ theorem pair_unpair (n : ℕ) : pair (unpair n).1 (unpair n).2 = n := by
       (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
     simp [s, pair, hl.not_lt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]
 
-theorem pair_unpair' {n a b} (H : unpair n = (a, b)) : pair a b = n := by
+theorem pair_eq_of_unpair_eq {n a b} (H : unpair n = (a, b)) : pair a b = n := by
   simpa [H] using pair_unpair n
 
+@[deprecated (since := "2025-05-24")]
+alias pair_unpair' := pair_eq_of_unpair_eq
+
 @[simp]
 theorem unpair_pair (a b : ℕ) : unpair (pair a b) = (a, b) := by
   dsimp only [pair]; split_ifs with h

Mathlib/Data/Nat/Prime/Basic.lean

@@ -28,9 +28,12 @@ theorem prime_mul_iff {a b : ℕ} : Nat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨
 theorem not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b) := by
   simp [prime_mul_iff, _root_.not_or, *]
 
-theorem not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n :=
+theorem not_prime_of_mul_eq {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n :=
   h ▸ not_prime_mul h₁ h₂
 
+@[deprecated (since := "2025-05-24")]
+alias not_prime_mul' := not_prime_of_mul_eq
+
 theorem Prime.dvd_iff_eq {p a : ℕ} (hp : p.Prime) (a1 : a ≠ 1) : a ∣ p ↔ p = a := by
   refine ⟨?_, by rintro rfl; rfl⟩
   rintro ⟨j, rfl⟩

Mathlib/Logic/Equiv/List.lean

@@ -136,7 +136,7 @@ theorem denumerable_list_aux : ∀ n : ℕ, ∃ a ∈ @decodeList α _ n, encode
       ⟨a, h₁, h₂⟩
     rw [Option.mem_def] at h₁
     use ofNat α v₁ :: a
-    simp [decodeList, e, h₂, h₁, encodeList, pair_unpair' e]
+    simp [decodeList, e, h₂, h₁, encodeList, pair_eq_of_unpair_eq e]
 
 /-- If `α` is denumerable, then so is `List α`. -/
 instance denumerableList : Denumerable (List α) :=

Mathlib/Order/Partition/Finpartition.lean

@@ -603,7 +603,7 @@ instance (s : Finset α) : Bot (Finpartition s) :=
       supIndep := Set.PairwiseDisjoint.supIndep <| by
         rw [Finset.coe_map]
         exact Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)
-      sup_parts := by rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton']
+      sup_parts := by rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]
       bot_notMem := by simp }⟩
 
 @[simp]

Mathlib/Tactic/NormNum/Prime.lean

@@ -30,7 +30,7 @@ namespace Mathlib.Meta.NormNum
 
 theorem not_prime_mul_of_ble (a b n : ℕ) (h : a * b = n) (h₁ : a.ble 1 = false)
     (h₂ : b.ble 1 = false) : ¬ n.Prime :=
-  not_prime_mul' h (ble_eq_false.mp h₁).ne' (ble_eq_false.mp h₂).ne'
+  not_prime_of_mul_eq h (ble_eq_false.mp h₁).ne' (ble_eq_false.mp h₂).ne'
 
 /-- Produce a proof that `n` is not prime from a factor `1 < d < n`. `en` should be the expression
   that is the natural number literal `n`. -/