chore(Algebra/Group/Support): rename primed lemmas to match naming convention (#27777)

`mulSupport_inv` should be called `mulSupport_fun_inv`, according to the [naming convention](https://leanprover-community.github.io/contribute/naming.html#unexpanded-and-expanded-forms-of-functions),
similarly for the other lemmas.

Unfortunately, there is no good tooling yet for renames `A -> B` and `B -> C`.

Author: grunweg

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -545,7 +545,7 @@ equals the product of `f i` divided by the product of `g i`. -/
       equals the sum of `f i` minus the sum of `g i`."]
 theorem finprod_div_distrib [DivisionCommMonoid G] {f g : α → G} (hf : (mulSupport f).Finite)
     (hg : (mulSupport g).Finite) : ∏ᶠ i, f i / g i = (∏ᶠ i, f i) / ∏ᶠ i, g i := by
-  simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_inv g).symm.rec hg),
+  simp only [div_eq_mul_inv, finprod_mul_distrib hf ((mulSupport_fun_inv g).symm.rec hg),
     finprod_inv_distrib]
 
 /-- A more general version of `finprod_mem_mul_distrib` that only requires `s ∩ mulSupport f` and

Mathlib/Algebra/Group/Indicator.lean

@@ -180,7 +180,7 @@ variable (M)
 
 @[to_additive (attr := simp)]
 theorem mulIndicator_one (s : Set α) : (mulIndicator s fun _ => (1 : M)) = fun _ => (1 : M) :=
-  mulIndicator_eq_one.2 <| by simp only [mulSupport_one, empty_disjoint]
+  mulIndicator_eq_one.2 <| by simp only [mulSupport_fun_one, empty_disjoint]
 
 @[to_additive (attr := simp)]
 theorem mulIndicator_one' {s : Set α} : s.mulIndicator (1 : α → M) = 1 :=

Mathlib/Algebra/Group/Support.lean

@@ -138,12 +138,15 @@ lemma range_eq_image_or_of_mulSupport_subset {f : α → M} {k : Set α} (h : mu
   grind
 
 @[to_additive (attr := simp)]
-theorem mulSupport_one' : mulSupport (1 : α → M) = ∅ :=
+theorem mulSupport_one : mulSupport (1 : α → M) = ∅ :=
   mulSupport_eq_empty_iff.2 rfl
 
 @[to_additive (attr := simp)]
-theorem mulSupport_one : (mulSupport fun _ : α => (1 : M)) = ∅ :=
-  mulSupport_one'
+theorem mulSupport_fun_one : (mulSupport fun _ : α => (1 : M)) = ∅ :=
+  mulSupport_one
+
+@[deprecated (since := "2025-07-31")] alias support_zero' := support_zero
+@[deprecated (since := "2025-07-31")] alias mulSupport_one' := mulSupport_one
 
 @[to_additive]
 theorem mulSupport_const {c : M} (hc : c ≠ 1) : (mulSupport fun _ : α => c) = Set.univ := by
@@ -179,16 +182,21 @@ theorem mulSupport_comp_eq_preimage (g : β → M) (f : α → β) :
     mulSupport (g ∘ f) = f ⁻¹' mulSupport g :=
   rfl
 
-@[to_additive support_prod_mk]
-theorem mulSupport_prod_mk (f : α → M) (g : α → N) :
+@[to_additive support_prodMk]
+theorem mulSupport_prodMk (f : α → M) (g : α → N) :
     (mulSupport fun x => (f x, g x)) = mulSupport f ∪ mulSupport g :=
   Set.ext fun x => by
     simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]
 
-@[to_additive support_prod_mk']
-theorem mulSupport_prod_mk' (f : α → M × N) :
+@[to_additive support_prodMk']
+theorem mulSupport_prodMk' (f : α → M × N) :
     mulSupport f = (mulSupport fun x => (f x).1) ∪ mulSupport fun x => (f x).2 := by
-  simp only [← mulSupport_prod_mk]
+  simp only [← mulSupport_prodMk]
+
+@[deprecated (since := "2025-07-31")] alias support_prod_mk := support_prodMk
+@[deprecated (since := "2025-07-31")] alias mulSupport_prod_mk := mulSupport_prodMk
+@[deprecated (since := "2025-07-31")] alias support_prod_mk' := support_prodMk'
+@[deprecated (since := "2025-07-31")] alias mulSupport_prod_mk' := mulSupport_prodMk'
 
 @[to_additive]
 theorem mulSupport_along_fiber_subset (f : α × β → M) (a : α) :
@@ -201,22 +209,25 @@ theorem mulSupport_curry (f : α × β → M) :
   simp [mulSupport, funext_iff, image]
 
 @[to_additive]
-theorem mulSupport_curry' (f : α × β → M) :
+theorem mulSupport_fun_curry (f : α × β → M) :
     (mulSupport fun a b ↦ f (a, b)) = (mulSupport f).image Prod.fst :=
   mulSupport_curry f
 
+@[deprecated (since := "2025-07-31")] alias support_curry' := support_fun_curry
+@[deprecated (since := "2025-07-31")] alias mulSupport_curry' := mulSupport_fun_curry
+
 end One
 
 @[to_additive]
 theorem mulSupport_mul [MulOneClass M] (f g : α → M) :
-    (mulSupport fun x => f x * g x) ⊆ mulSupport f ∪ mulSupport g :=
+    (mulSupport fun x ↦ f x * g x) ⊆ mulSupport f ∪ mulSupport g :=
   mulSupport_binop_subset (· * ·) (one_mul _) f g
 
 @[to_additive]
 theorem mulSupport_pow [Monoid M] (f : α → M) (n : ℕ) :
     (mulSupport fun x => f x ^ n) ⊆ mulSupport f := by
   induction n with
-  | zero => simp [pow_zero, mulSupport_one]
+  | zero => simp [pow_zero]
   | succ n hfn =>
     simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)
 
@@ -225,12 +236,15 @@ section DivisionMonoid
 variable [DivisionMonoid G] (f g : α → G)
 
 @[to_additive (attr := simp)]
-theorem mulSupport_inv : (mulSupport fun x => (f x)⁻¹) = mulSupport f :=
+theorem mulSupport_fun_inv : (mulSupport fun x => (f x)⁻¹) = mulSupport f :=
   ext fun _ => inv_ne_one
 
 @[to_additive (attr := simp)]
-theorem mulSupport_inv' : mulSupport f⁻¹ = mulSupport f :=
-  mulSupport_inv f
+theorem mulSupport_inv : mulSupport f⁻¹ = mulSupport f :=
+  mulSupport_fun_inv f
+
+@[deprecated (since := "2025-07-31")] alias support_neg' := support_neg
+@[deprecated (since := "2025-07-31")] alias mulSupport_inv' := mulSupport_inv
 
 @[to_additive]
 theorem mulSupport_mul_inv : (mulSupport fun x => f x * (g x)⁻¹) ⊆ mulSupport f ∪ mulSupport g :=

Mathlib/Algebra/GroupWithZero/Indicator.lean

@@ -158,7 +158,7 @@ lemma mulSupport_add_one' [AddRightCancelMonoid R] (f : ι → R) : mulSupport (
   mulSupport_add_one f
 
 lemma mulSupport_one_sub' [AddGroup R] (f : ι → R) : mulSupport (1 - f) = support f := by
-  rw [sub_eq_add_neg, mulSupport_one_add', support_neg']
+  rw [sub_eq_add_neg, mulSupport_one_add', support_neg]
 
 lemma mulSupport_one_sub [AddGroup R] (f : ι → R) :
     mulSupport (fun x ↦ 1 - f x) = support f := mulSupport_one_sub' f

Mathlib/LinearAlgebra/RootSystem/Base.lean

@@ -196,7 +196,7 @@ lemma pos_or_neg_of_sum_smul_root_mem (f : ι → ℤ)
     have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [hk]
     rcases b.root_mem_or_neg_mem k with hk' | hk' <;> rw [hk] at hk'
     · left; exact this f hk' hf₀ hf'
-    · right; simpa using this (-f) (by convert hk'; simp) (by simpa only [support_neg']) (by simpa)
+    · right; simpa using this (-f) (by convert hk'; simp) (by simpa only [support_neg]) (by simpa)
   intro f hf hf₀ hf'
   let f' : b.support → ℤ := fun i ↦ f i
   replace hf : ∑ j, f' j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support) := by

Mathlib/MeasureTheory/Function/SimpleFunc.lean

@@ -1197,7 +1197,7 @@ theorem map_iff {g : β → γ} (hg : ∀ {b}, g b = 0 ↔ b = 0) :
 protected theorem pair {g : α →ₛ γ} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) :
     (pair f g).FinMeasSupp μ :=
   calc
-    μ (support <| pair f g) = μ (support f ∪ support g) := congr_arg μ <| support_prod_mk f g
+    μ (support <| pair f g) = μ (support f ∪ support g) := congr_arg μ <| support_prodMk f g
     _ ≤ μ (support f) + μ (support g) := measure_union_le _ _
     _ < _ := add_lt_top.2 ⟨hf, hg⟩
 

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -1048,7 +1048,7 @@ end StronglyMeasurable
 theorem finStronglyMeasurable_zero {α β} {m : MeasurableSpace α} {μ : Measure α} [Zero β]
     [TopologicalSpace β] : FinStronglyMeasurable (0 : α → β) μ :=
   ⟨0, by
-    simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero', measure_empty,
+    simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero, measure_empty,
       zero_lt_top, forall_const],
     fun _ => tendsto_const_nhds⟩
 
@@ -1132,9 +1132,9 @@ protected theorem add [AddZeroClass β] [ContinuousAdd β] (hf : FinStronglyMeas
 @[measurability]
 protected theorem neg [SubtractionMonoid β] [ContinuousNeg β] (hf : FinStronglyMeasurable f μ) :
     FinStronglyMeasurable (-f) μ := by
-  refine ⟨fun n => -hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).neg⟩
-  suffices μ (Function.support fun x => -(hf.approx n) x) < ∞ by convert this
-  rw [Function.support_neg (hf.approx n)]
+  refine ⟨fun n ↦ -hf.approx n, fun n ↦ ?_, fun x ↦ (hf.tendsto_approx x).neg⟩
+  suffices μ (Function.support fun x ↦ -(hf.approx n) x) < ∞ by convert this
+  rw [Function.support_fun_neg (hf.approx n)]
   exact hf.fin_support_approx n
 
 @[measurability]

Mathlib/RingTheory/HahnSeries/Addition.lean

@@ -343,7 +343,7 @@ instance : Neg (HahnSeries Γ R) where
   neg x :=
     { coeff := fun a => -x.coeff a
       isPWO_support' := by
-        rw [Function.support_neg]
+        rw [Function.support_fun_neg]
         exact x.isPWO_support }
 
 @[simp]

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -155,7 +155,7 @@ def toIterate [PartialOrder Γ'] (x : HahnSeries (Γ ×ₗ Γ') R) :
         (Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g)) = Function.support
         fun g => fun g' => x.coeff (g, g') := by
       simp only [Function.support, ne_eq, mk_eq_zero]
-    rw [h₁, Function.support_curry' x.coeff]
+    rw [h₁, Function.support_fun_curry x.coeff]
     exact Set.PartiallyWellOrderedOn.imageProdLex x.isPWO_support'
 
 /-- The equivalence between iterated Hahn series and Hahn series on the lex product. -/
@@ -491,7 +491,7 @@ theorem forallLTEqZero_supp_BddBelow (f : Γ → R) (n : Γ) (hn : ∀ (m : Γ),
   exact not_lt.mp (mt (hn m) hm)
 
 theorem BddBelow_zero [Nonempty Γ] : BddBelow (Function.support (0 : Γ → R)) := by
-  simp only [support_zero', bddBelow_empty]
+  simp only [Function.support_zero, bddBelow_empty]
 
 variable [LocallyFiniteOrder Γ]
 

Mathlib/Topology/Algebra/Support.lean

@@ -333,7 +333,7 @@ section DivisionMonoid
 protected lemma HasCompactMulSupport.inv {α β : Type*} [TopologicalSpace α] [DivisionMonoid β]
     {f : α → β} (hf : HasCompactMulSupport f) :
     HasCompactMulSupport (f⁻¹) := by
-  simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv'] using hf
+  simpa only [HasCompactMulSupport, mulTSupport, mulSupport_inv] using hf
 
 @[deprecated (since := "2025-07-31")] alias HasCompactSupport.neg' := HasCompactSupport.neg
 @[deprecated (since := "2025-07-31")] alias HasCompactMulSupport.inv' := HasCompactMulSupport.inv