refactor: rename restrict to domRestrict (leanprover-community#25980)

Update the documentation for consistency, and to contrast with `codRestrict` which is prevalent.

Author: Multramate

Archive/Sensitivity.lean

@@ -387,12 +387,12 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     rw [rank_range_of_injective (g m) g_injective]
     apply dim_V
   have dimW : dim W = card H := by
-    have li : LinearIndependent ℝ (H.restrict e) := by
+    have li : LinearIndependent ℝ (H.domRestrict e) := by
       convert! (dualBases_e_ε m.succ).basis.linearIndependent.comp _ Subtype.val_injective
       rw [(dualBases_e_ε _).coe_basis]
       rfl
     have hdW := rank_span li
-    rw [Set.range_restrict] at hdW
+    rw [Set.range_domRestrict] at hdW
     convert! hdW
     rw [← (dualBases_e_ε _).coe_basis, Cardinal.mk_image_eq (dualBases_e_ε _).basis.injective,
       Cardinal.mk_fintype]

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1087,20 +1087,20 @@ theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg
   have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
     rintro ⟨x, hx⟩
     exact hn.conj_mem _ hx c
-  have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.restrict N).codRestrict _ h) := by
+  have hs : Function.Surjective (((MulAut.conj c).toMonoidHom.domRestrict N).codRestrict _ h) := by
     rintro ⟨x, hx⟩
     refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
     · have h := hn.conj_mem _ hx c⁻¹
       rwa [inv_inv] at h
     simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
-      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
+      MonoidHom.domRestrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
     rw [mul_assoc, mul_inv_cancel, mul_one]
   rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]
   grw [eq_top_iff.1 ht]
   refine map_le_iff_le_comap.2 (normalClosure_le_normal ?_)
   rw [Set.singleton_subset_iff, SetLike.mem_coe]
   simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
-    MonoidHom.restrict_apply, mem_comap]
+    MonoidHom.domRestrict_apply, mem_comap]
   exact subset_normalClosure (Set.mem_singleton _)
 
 end IsConj

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -94,10 +94,14 @@ instance _root_.Subgroup.range_isMulCommutative {G : Type*} [Group G] [IsMulComm
   range_eq_map f ▸ Subgroup.map_isMulCommutative ⊤ f
 
 @[to_additive (attr := simp)]
-theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
-  simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
+theorem domRestrict_range (f : G →* N) : (f.domRestrict K).range = K.map f := by
+  simp_rw [SetLike.ext_iff, mem_range, mem_map, domRestrict_apply, SetLike.exists,
     exists_prop, forall_const]
 
+@[deprecated (since := "2026-07-19")] alias restrict_range := domRestrict_range
+@[deprecated (since := "2026-07-19")]
+alias _root_.AddMonoidHom.restrict_range := _root_.AddMonoidHom.domRestrict_range
+
 /-- The canonical surjective group homomorphism `G →* f(G)` induced by a group
 homomorphism `G →* N`. -/
 @[to_additive
@@ -280,9 +284,13 @@ theorem ker_le_comap (f : G →* N) (H : Subgroup N) : f.ker ≤ H.comap f :=
   comap_mono bot_le
 
 @[to_additive (attr := simp)]
-theorem ker_restrict (f : G →* M) : (f.restrict K).ker = f.ker.subgroupOf K :=
+theorem ker_domRestrict (f : G →* M) : (f.domRestrict K).ker = f.ker.subgroupOf K :=
   rfl
 
+@[deprecated (since := "2026-07-19")] alias ker_restrict := ker_domRestrict
+@[deprecated (since := "2026-07-19")]
+alias _root_.AddMonoidHom.ker_restrict := _root_.AddMonoidHom.ker_domRestrict
+
 @[to_additive (attr := simp)]
 theorem ker_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S)
     (h : ∀ x, f x ∈ s) : (f.codRestrict s h).ker = f.ker :=

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -50,7 +50,7 @@ In this file we define various operations on `Subsemigroup`s and `MulHom`s.
 ### Operations on `MulHom`s
 
 * `MulHom.srange`: range of a semigroup homomorphism as a subsemigroup of the codomain;
-* `MulHom.restrict`: restrict a semigroup homomorphism to a subsemigroup;
+* `MulHom.domRestrict`: restrict a semigroup homomorphism to a subsemigroup of its domain;
 * `MulHom.codRestrict`: restrict the codomain of a semigroup homomorphism to a subsemigroup;
 * `MulHom.srangeRestrict`: restrict a semigroup homomorphism to its range;
 
@@ -595,14 +595,21 @@ theorem map_mclosure (f : M →ₙ* N) (s : Set M) : (closure s).map f = closure
 
 /-- Restriction of a semigroup hom to a subsemigroup of the domain. -/
 @[to_additive /-- Restriction of an AddSemigroup hom to an `AddSubsemigroup` of the domain. -/]
-def restrict {N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) (S : σ) : S →ₙ* N :=
+def domRestrict {N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N)
+    (S : σ) : S →ₙ* N :=
   f.comp (MulMemClass.subtype S)
 
 @[to_additive (attr := simp)]
-theorem restrict_apply {N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) {S : σ}
-    (x : S) : f.restrict S x = f x :=
+theorem domRestrict_apply {N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M]
+    (f : M →ₙ* N) {S : σ} (x : S) : f.domRestrict S x = f x :=
   rfl
 
+@[deprecated (since := "2026-07-19")] alias restrict := domRestrict
+@[deprecated (since := "2026-07-19")] alias _root_.AddHom.restrict := _root_.AddHom.domRestrict
+@[deprecated (since := "2026-07-19")] alias restrict_apply := domRestrict_apply
+@[deprecated (since := "2026-07-19")]
+alias _root_.AddHom.restrict_apply := _root_.AddHom.domRestrict_apply
+
 /-- Restriction of a semigroup hom to a subsemigroup of the codomain. -/
 @[to_additive (attr := simps)
   /-- Restriction of an `AddSemigroup` hom to an `AddSubsemigroup` of the codomain. -/]

Mathlib/Algebra/Group/Subsemigroup/Operations.lean

@@ -148,7 +148,7 @@ theorem domRestrict_apply (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (
   rfl
 
 lemma coe_domRestrict (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :
-    ⇑(f.domRestrict p) = Set.restrict p f := rfl
+    ⇑(f.domRestrict p) = Set.domRestrict p f := rfl
 
 /-- A linear map `f : M₂ → M` whose values lie in a submodule `p ⊆ M` can be restricted to a
 linear map M₂ → p.

Mathlib/Algebra/Module/Submodule/LinearMap.lean

@@ -400,9 +400,11 @@ def domRestrict (f : R →+* S) (s : σR) : s →+* S :=
   f.comp <| SubsemiringClass.subtype s
 
 @[simp]
-theorem restrict_apply (f : R →+* S) {s : σR} (x : s) : f.domRestrict s x = f x :=
+theorem domRestrict_apply (f : R →+* S) {s : σR} (x : s) : f.domRestrict s x = f x :=
   rfl
 
+@[deprecated (since := "2026-07-19")] alias restrict_apply := domRestrict_apply
+
 /-- The subsemiring of elements `x : R` such that `f x = g x` -/
 def eqLocusS (f g : R →+* S) : Subsemiring R :=
   { (f : R →* S).eqLocusM g, (f : R →+ S).eqLocusM g with carrier := { x | f x = g x } }

Mathlib/Algebra/Ring/Subsemiring/Defs.lean

@@ -78,7 +78,7 @@ protected theorem Commute.cfc {a b : A} (hb₁ : Commute a b)
     (hb₂ : Commute (star a) b) (f : 𝕜 → 𝕜) :
     Commute (cfc f a) b :=
   cfc_cases (fun x ↦ Commute x b) a f (Commute.zero_left _)
-    fun hf ha ↦ hb₁.cfcHom ha hb₂ ⟨_, hf.restrict⟩
+    fun hf ha ↦ hb₁.cfcHom ha hb₂ ⟨_, hf.domRestrict⟩
 
 /-- For `a` selfadjoint, an element commutes with `cfc f a` if it commutes with `a`.
 
@@ -163,7 +163,7 @@ protected theorem Commute.cfcₙ {a b : A} (hb₁ : Commute a b)
     (hb₂ : Commute (star a) b) (f : 𝕜 → 𝕜) :
     Commute (cfcₙ f a) b :=
   cfcₙ_cases (fun x ↦ Commute x b) a f (Commute.zero_left _)
-    fun hf hf₀ ha ↦ hb₁.cfcₙHom ha hb₂ ⟨⟨_, hf.restrict⟩, hf₀⟩
+    fun hf hf₀ ha ↦ hb₁.cfcₙHom ha hb₂ ⟨⟨_, hf.domRestrict⟩, hf₀⟩
 
 /-- For `a` selfadjoint, an element commutes with `cfcₙ f a` if it commutes with `a`.
 

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Commute.lean

@@ -96,7 +96,7 @@ theorem tendsto_cfc_fun {l : Filter X} {F : X → R → R} {f : R → R} {a : A}
       rw [Function.comp_apply, cfc_apply (hf := x.2)]
     rw [cfc_apply ..]
     apply cfcHom_continuous _ |>.tendsto _ |>.comp
-    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn Subtype.property]
+    rw [hf.tendsto_domRestrict_iff_tendstoUniformlyOn Subtype.property]
     intro t
     simp only [eventually_comap, Subtype.forall]
     peel h_tendsto t with ht x _
@@ -235,12 +235,13 @@ satisfying the predicate `p` (associated to `𝕜`) and whose `𝕜`-spectrum is
 theorem continuousOn_cfc {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜)
     (hf : ContinuousOn f s := by cfc_cont_tac) :
     ContinuousOn (cfc f) {a | p a ∧ spectrum 𝕜 a ⊆ s} :=
-  continuousOn_iff_continuous_restrict.mpr <| by
+  continuousOn_iff_continuous_domRestrict.mpr <| by
     convert!
-      continuous_cfcHomSuperset_left hs ⟨_, hf.restrict⟩ ((↑) : {a | p a ∧ spectrum 𝕜 a ⊆ s} → A)
+      continuous_cfcHomSuperset_left hs ⟨_, hf.domRestrict⟩
+        ((↑) : {a | p a ∧ spectrum 𝕜 a ⊆ s} → A)
         continuous_subtype_val (fun x ↦ x.2.2) with
       x
-    rw [cfcHomSuperset_apply, Set.restrict_apply, cfc_apply _ _ x.2.1 (hf.mono x.2.2)]
+    rw [cfcHomSuperset_apply, Set.domRestrict_apply, cfc_apply _ _ x.2.1 (hf.mono x.2.2)]
     congr!
 
 open UniformOnFun in
@@ -626,9 +627,9 @@ theorem tendsto_cfcₙ_fun {l : Filter X} {F : X → R → R} {f : R → R} {a :
     rw [cfcₙ_apply ..]
     apply cfcₙHom_continuous _ |>.tendsto _ |>.comp
     rw [ContinuousMapZero.isEmbedding_toContinuousMap.isInducing.tendsto_nhds_iff]
-    change Tendsto (fun x : s ↦ (⟨_, x.2.1.restrict⟩ : C(quasispectrum R a, R))) _
-      (𝓝 ⟨_, hf.restrict⟩)
-    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn (fun x ↦ x.2.1)]
+    change Tendsto (fun x : s ↦ (⟨_, x.2.1.domRestrict⟩ : C(quasispectrum R a, R))) _
+      (𝓝 ⟨_, hf.domRestrict⟩)
+    rw [hf.tendsto_domRestrict_iff_tendstoUniformlyOn (fun x ↦ x.2.1)]
     intro t
     simp only [eventually_comap, Subtype.forall]
     peel h_tendsto t with ht x _
@@ -771,12 +772,12 @@ theorem continuousOn_cfcₙ {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜
     (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) :
     ContinuousOn (cfcₙ f · : A → A) {a | p a ∧ quasispectrum 𝕜 a ⊆ s} := by
   by_cases hs0 : 0 ∈ s
-  · rw [continuousOn_iff_continuous_restrict]
+  · rw [continuousOn_iff_continuous_domRestrict]
     convert!
-      continuous_cfcₙHomSuperset_left hs (hs0 := ⟨hs0⟩) ⟨⟨_, hf.restrict⟩, hf0⟩ (X :=
+      continuous_cfcₙHomSuperset_left hs (hs0 := ⟨hs0⟩) ⟨⟨_, hf.domRestrict⟩, hf0⟩ (X :=
         {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}) continuous_subtype_val (fun x ↦ x.2.2) with
       x
-    rw [cfcₙHomSuperset_apply, Set.restrict_apply, cfcₙ_apply _ _ (hf.mono x.2.2) hf0 x.2.1]
+    rw [cfcₙHomSuperset_apply, Set.domRestrict_apply, cfcₙ_apply _ _ (hf.mono x.2.2) hf0 x.2.1]
     congr!
   · convert! continuousOn_empty _
     rw [Set.eq_empty_iff_forall_notMem]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean

@@ -74,7 +74,7 @@ For a version with stronger assumptions which in practice are often easier to ve
 `integrable_cfc`. -/
 lemma integrable_cfc' (f : X → 𝕜 → 𝕜) (a : A)
     (hf : Integrable
-      (fun x : X => mkD ((spectrum 𝕜 a).restrict (f x)) 0) μ)
+      (fun x : X => mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ)
     (ha : p a := by cfc_tac) :
     Integrable (fun x => cfc (f x) a) μ := by
   conv in cfc _ _ => rw [cfc_eq_cfcL_mkD _ a]
@@ -85,7 +85,7 @@ For a version with stronger assumptions which in practice are often easier to ve
 `integrableOn_cfc`. -/
 lemma integrableOn_cfc' {s : Set X} (f : X → 𝕜 → 𝕜) (a : A)
     (hf : IntegrableOn
-      (fun x : X => mkD ((spectrum 𝕜 a).restrict (f x)) 0) s μ)
+      (fun x : X => mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) s μ)
     (ha : p a := by cfc_tac) :
     IntegrableOn (fun x => cfc (f x) a) s μ := by
   exact integrable_cfc' _ _ hf ha
@@ -130,21 +130,21 @@ For a version with stronger assumptions which in practice are often easier to ve
 lemma cfc_integral' [NormedSpace ℝ A] (f : X → 𝕜 → 𝕜) (a : A)
     (hf₁ : ∀ᵐ x ∂μ, ContinuousOn (f x) (spectrum 𝕜 a))
     (hf₂ : Integrable
-      (fun x : X => mkD ((spectrum 𝕜 a).restrict (f x)) 0) μ)
+      (fun x : X => mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ)
     (ha : p a := by cfc_tac) :
     cfc (fun z => ∫ x, f x z ∂μ) a = ∫ x, cfc (f x) a ∂μ := by
   have key₁ (z : spectrum 𝕜 a) :
-      ∫ x, f x z ∂μ = (∫ x, mkD ((spectrum 𝕜 a).restrict (f x)) 0 ∂μ) z := by
+      ∫ x, f x z ∂μ = (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
     rw [integral_apply hf₂]
     refine integral_congr_ae ?_
     filter_upwards [hf₁] with x cont_x
     rw [mkD_apply_of_continuousOn cont_x]
   have key₂ (z : spectrum 𝕜 a) :
-      ∫ x, f x z ∂μ = mkD ((spectrum 𝕜 a).restrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
+      ∫ x, f x z ∂μ = mkD ((spectrum 𝕜 a).domRestrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
     rw [mkD_apply_of_continuousOn]
-    rw [continuousOn_iff_continuous_restrict]
+    rw [continuousOn_iff_continuous_domRestrict]
     refine continuous_congr key₁ |>.mpr ?_
-    exact map_continuous (∫ x, mkD ((spectrum 𝕜 a).restrict (f x)) 0 ∂μ)
+    exact map_continuous (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)
   simp_rw [cfc_eq_cfcL_mkD _ a, cfcL_integral a _ hf₂ ha]
   congr
   ext z
@@ -157,7 +157,7 @@ For a version with stronger assumptions which in practice are often easier to ve
 lemma cfc_setIntegral' {s : Set X} [NormedSpace ℝ A] (f : X → 𝕜 → 𝕜) (a : A)
     (hf₁ : ∀ᵐ x ∂(μ.restrict s), ContinuousOn (f x) (spectrum 𝕜 a))
     (hf₂ : IntegrableOn
-      (fun x : X => mkD ((spectrum 𝕜 a).restrict (f x)) 0) s μ)
+      (fun x : X => mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) s μ)
     (ha : p a := by cfc_tac) :
     cfc (fun z => ∫ x in s, f x z ∂μ) a = ∫ x in s, cfc (f x) a ∂μ :=
   cfc_integral' _ _ hf₁ hf₂ ha
@@ -228,7 +228,7 @@ For a version with stronger assumptions which in practice are often easier to ve
 `integrable_cfcₙ`. -/
 lemma integrable_cfcₙ' (f : X → 𝕜 → 𝕜) (a : A)
     (hf : Integrable
-      (fun x : X => mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) μ)
+      (fun x : X => mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ)
     (ha : p a := by cfc_tac) :
     Integrable (fun x => cfcₙ (f x) a) μ := by
   conv in cfcₙ _ _ => rw [cfcₙ_eq_cfcₙL_mkD _ a]
@@ -239,7 +239,7 @@ For a version with stronger assumptions which in practice are often easier to ve
 `integrableOn_cfcₙ`. -/
 lemma integrableOn_cfcₙ' {s : Set X} (f : X → 𝕜 → 𝕜) (a : A)
     (hf : IntegrableOn
-      (fun x : X => mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) s μ)
+      (fun x : X => mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) s μ)
     (ha : p a := by cfc_tac) :
     IntegrableOn (fun x => cfcₙ (f x) a) s μ := by
   exact integrable_cfcₙ' _ _ hf ha
@@ -288,21 +288,21 @@ lemma cfcₙ_integral' [NormedSpace ℝ A] (f : X → 𝕜 → 𝕜) (a : A)
     (hf₁ : ∀ᵐ x ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a))
     (hf₂ : ∀ᵐ x ∂μ, f x 0 = 0)
     (hf₃ : Integrable
-      (fun x : X => mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) μ)
+      (fun x : X => mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ)
     (ha : p a := by cfc_tac) :
     cfcₙ (fun z => ∫ x, f x z ∂μ) a = ∫ x, cfcₙ (f x) a ∂μ := by
   have key₁ (z : quasispectrum 𝕜 a) :
-      ∫ x, f x z ∂μ = (∫ x, mkD ((quasispectrum 𝕜 a).restrict (f x)) 0 ∂μ) z := by
+      ∫ x, f x z ∂μ = (∫ x, mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
     rw [integral_apply hf₃]
     refine integral_congr_ae ?_
     filter_upwards [hf₁, hf₂] with x cont_x zero_x
     rw [mkD_apply_of_continuousOn cont_x zero_x]
   have key₂ (z : quasispectrum 𝕜 a) :
-      ∫ x, f x z ∂μ = mkD ((quasispectrum 𝕜 a).restrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
+      ∫ x, f x z ∂μ = mkD ((quasispectrum 𝕜 a).domRestrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
     rw [mkD_apply_of_continuousOn]
-    · rw [continuousOn_iff_continuous_restrict]
+    · rw [continuousOn_iff_continuous_domRestrict]
       refine continuous_congr key₁ |>.mpr ?_
-      exact map_continuous (∫ x, mkD ((quasispectrum 𝕜 a).restrict (f x)) 0 ∂μ)
+      exact map_continuous (∫ x, mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)
     · exact integral_eq_zero_of_ae hf₂
   simp_rw [cfcₙ_eq_cfcₙL_mkD _ a, cfcₙL_integral a _ hf₃ ha]
   congr
@@ -317,7 +317,7 @@ lemma cfcₙ_setIntegral' {s : Set X} [NormedSpace ℝ A] (f : X → 𝕜 → 
     (hf₁ : ∀ᵐ x ∂(μ.restrict s), ContinuousOn (f x) (quasispectrum 𝕜 a))
     (hf₂ : ∀ᵐ x ∂(μ.restrict s), f x 0 = 0)
     (hf₃ : IntegrableOn
-      (fun x : X => mkD ((quasispectrum 𝕜 a).restrict (f x)) 0) s μ)
+      (fun x : X => mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) s μ)
     (ha : p a := by cfc_tac) :
     cfcₙ (fun z => ∫ x in s, f x z ∂μ) a = ∫ x in s, cfcₙ (f x) a ∂μ :=
   cfcₙ_integral' _ _ hf₁ hf₂ hf₃ ha