refactor(algebra/sub{monoid,group,ring,semiring,field}): merge togeth…

…er the `restrict` and `cod_restrict` helpers (#14548)

This uses the new subobject typeclasses to merge together:
* `monoid_hom.mrestrict`, `monoid_hom.restrict`
* `monoid_hom.cod_mrestrict`, `monoid_hom.cod_restrict`
* `ring_hom.srestrict`, `ring_hom.restrict`, `ring_hom.restrict_field`
* `ring_hom.cod_srestrict`, `ring_hom.cod_restrict`, `ring_hom.cod_restrict_field`

For consistency, this also removes the `m` prefix from `mul_hom.mrestrict`

src/algebra/algebra/subalgebra/basic.lean

@@ -245,7 +245,7 @@ instance algebra' [comm_semiring R'] [has_scalar R' R] [algebra R' A]
   [is_scalar_tower R' R A] : algebra R' S :=
 { commutes' := λ c x, subtype.eq $ algebra.commutes _ _,
   smul_def' := λ c x, subtype.eq $ algebra.smul_def _ _,
-  .. (algebra_map R' A).cod_srestrict S.to_subsemiring $ λ x, begin
+  .. (algebra_map R' A).cod_restrict S $ λ x, begin
     rw [algebra.algebra_map_eq_smul_one, ←smul_one_smul R x (1 : A),
       ←algebra.algebra_map_eq_smul_one],
     exact algebra_map_mem S _,
@@ -434,7 +434,7 @@ set_like.coe_mono (set.range_comp_subset_range f g)
 /-- Restrict the codomain of an algebra homomorphism. -/
 def cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) : A →ₐ[R] S :=
 { commutes' := λ r, subtype.eq $ f.commutes r,
-  .. ring_hom.cod_srestrict (f : A →+* B) S.to_subsemiring hf }
+  .. ring_hom.cod_restrict (f : A →+* B) S hf }
 
 @[simp] lemma val_comp_cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) :
   S.val.comp (f.cod_restrict S hf) = f :=

src/algebra/category/Ring/constructions.lean

@@ -166,7 +166,7 @@ def equalizer_fork_is_limit : is_limit (equalizer_fork f g) :=
 begin
   fapply fork.is_limit.mk',
   intro s,
-  use s.ι.cod_restrict' _ (λ x, (concrete_category.congr_hom s.condition x : _)),
+  use s.ι.cod_restrict _ (λ x, (concrete_category.congr_hom s.condition x : _)),
   split,
   { ext, refl },
   { intros m hm, ext x, exact concrete_category.congr_hom hm x }

src/field_theory/subfield.lean

@@ -600,20 +600,6 @@ variables {s : subfield K}
 
 open subfield
 
-/-- Restrict the codomain of a ring homomorphism to a subfield that includes the range. -/
-def cod_restrict_field (f : K →+* L)
-  (s : subfield L) (h : ∀ x, f x ∈ s) : K →+* s :=
-{ to_fun := λ x, ⟨f x, h x⟩,
-  map_add' := λ x y, subtype.eq $ f.map_add x y,
-  map_zero' := subtype.eq f.map_zero,
-  map_mul' := λ x y, subtype.eq $ f.map_mul x y,
-  map_one' := subtype.eq f.map_one }
-
-/-- Restriction of a ring homomorphism to a subfield of the domain. -/
-def restrict_field (f : K →+* L) (s : subfield K) : s →+* L := f.comp s.subtype
-
-@[simp] lemma restrict_field_apply (f : K →+* L) (x : s) : f.restrict_field s x = f x := rfl
-
 /-- Restriction of a ring homomorphism to its range interpreted as a subfield. -/
 def range_restrict_field (f : K →+* L) : K →+* f.field_range :=
 f.srange_restrict
@@ -661,7 +647,7 @@ open ring_hom
 
 /-- The ring homomorphism associated to an inclusion of subfields. -/
 def inclusion {S T : subfield K} (h : S ≤ T) : S →+* T :=
-S.subtype.cod_restrict_field _ (λ x, h x.2)
+S.subtype.cod_restrict _ (λ x, h x.2)
 
 @[simp] lemma field_range_subtype (s : subfield K) : s.subtype.field_range = s :=
 set_like.ext' $ (coe_srange _).trans subtype.range_coe

src/group_theory/free_product.lean

@@ -139,11 +139,11 @@ lemma induction_on {C : free_product M → Prop}
   C m :=
 begin
   let S : submonoid (free_product M) := submonoid.mk (set_of C) h_mul h_one,
-  convert subtype.prop (lift (λ i, of.cod_mrestrict S (h_of i)) m),
+  convert subtype.prop (lift (λ i, of.cod_restrict S (h_of i)) m),
   change monoid_hom.id _ m = S.subtype.comp _ m,
   congr,
   ext,
-  simp [monoid_hom.cod_mrestrict],
+  simp [monoid_hom.cod_restrict],
 end
 
 lemma of_left_inverse [decidable_eq ι] (i : ι) :

src/group_theory/monoid_localization.lean

@@ -462,16 +462,16 @@ by rw [mul_comm, sec_spec]
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `w : M, z : N` and `y ∈ S`, we have `w - f y = z ↔ w = f y + z`."]
 lemma mul_inv_left {f : M →* N} (h : ∀ y : S, is_unit (f y))
-  (y : S) (w z) : w * ↑(is_unit.lift_right (f.mrestrict S) h y)⁻¹ = z ↔ w = f y * z :=
+  (y : S) (w z) : w * ↑(is_unit.lift_right (f.restrict S) h y)⁻¹ = z ↔ w = f y * z :=
 by rw mul_comm; convert units.inv_mul_eq_iff_eq_mul _;
-  exact (is_unit.coe_lift_right (f.mrestrict S) h _).symm
+  exact (is_unit.coe_lift_right (f.restrict S) h _).symm
 
 /-- Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
 `w : M, z : N` and `y ∈ S`, we have `z = w * (f y)⁻¹ ↔ z * f y = w`. -/
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `w : M, z : N` and `y ∈ S`, we have `z = w - f y ↔ z + f y = w`."]
 lemma mul_inv_right {f : M →* N} (h : ∀ y : S, is_unit (f y))
-  (y : S) (w z) : z = w * ↑(is_unit.lift_right (f.mrestrict S) h y)⁻¹ ↔ z * f y = w :=
+  (y : S) (w z) : z = w * ↑(is_unit.lift_right (f.restrict S) h y)⁻¹ ↔ z * f y = w :=
 by rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
 
 /-- Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that
@@ -481,8 +481,8 @@ by rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]
 `f(S) ⊆ add_units N`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
 `f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁)`."]
 lemma mul_inv {f : M →* N} (h : ∀ y : S, is_unit (f y)) {x₁ x₂} {y₁ y₂ : S} :
-  f x₁ * ↑(is_unit.lift_right (f.mrestrict S) h y₁)⁻¹ =
-    f x₂ * ↑(is_unit.lift_right (f.mrestrict S) h y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁) :=
+  f x₁ * ↑(is_unit.lift_right (f.restrict S) h y₁)⁻¹ =
+    f x₂ * ↑(is_unit.lift_right (f.restrict S) h y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁) :=
 by rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ←mul_assoc, mul_inv_left h, mul_comm x₂,
   f.map_mul, f.map_mul]
 
@@ -491,17 +491,17 @@ by rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ←mul_assoc, mul_inv_le
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `y, z ∈ S`, we have `- (f y) = - (f z) → f y = f z`."]
 lemma inv_inj {f : M →* N} (hf : ∀ y : S, is_unit (f y)) {y z}
-  (h : (is_unit.lift_right (f.mrestrict S) hf y)⁻¹ = (is_unit.lift_right (f.mrestrict S) hf z)⁻¹) :
+  (h : (is_unit.lift_right (f.restrict S) hf y)⁻¹ = (is_unit.lift_right (f.restrict S) hf z)⁻¹) :
   f y = f z :=
 by rw [←mul_one (f y), eq_comm, ←mul_inv_left hf y (f z) 1, h];
-  convert units.inv_mul _; exact (is_unit.coe_lift_right (f.mrestrict S) hf _).symm
+  convert units.inv_mul _; exact (is_unit.coe_lift_right (f.restrict S) hf _).symm
 
 /-- Given a monoid hom `f : M →* N` and submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
 `y ∈ S`, `(f y)⁻¹` is unique. -/
 @[to_additive "Given an add_monoid hom `f : M →+ N` and submonoid `S ⊆ M` such that
 `f(S) ⊆ add_units N`, for all `y ∈ S`, `- (f y)` is unique."]
 lemma inv_unique {f : M →* N} (h : ∀ y : S, is_unit (f y)) {y : S}
-  {z} (H : f y * z = 1) : ↑(is_unit.lift_right (f.mrestrict S) h y)⁻¹ = z :=
+  {z} (H : f y * z = 1) : ↑(is_unit.lift_right (f.restrict S) h y)⁻¹ = z :=
 by rw [←one_mul ↑(_)⁻¹, mul_inv_left, ←H]
 
 variables (f : localization_map S N)
@@ -524,7 +524,7 @@ f.map_right_cancel $ by rw [mul_comm _ x, mul_comm _ y, h]
 @[to_additive "Given a localization map `f : M →+ N`, the surjection sending `(x, y) : M × S`
 to `f x - f y`."]
 noncomputable def mk' (f : localization_map S N) (x : M) (y : S) : N :=
-f.to_map x * ↑(is_unit.lift_right (f.to_map.mrestrict S) f.map_units y)⁻¹
+f.to_map x * ↑(is_unit.lift_right (f.to_map.restrict S) f.map_units y)⁻¹
 
 @[to_additive] lemma mk'_mul (x₁ x₂ : M) (y₁ y₂ : S) :
   f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂ :=
@@ -631,9 +631,9 @@ by rw [mul_comm, mk'_mul_cancel_right]
 
 @[to_additive] lemma is_unit_comp (j : N →* P) (y : S) :
   is_unit (j.comp f.to_map y) :=
-⟨units.map j $ is_unit.lift_right (f.to_map.mrestrict S) f.map_units y,
+⟨units.map j $ is_unit.lift_right (f.to_map.restrict S) f.map_units y,
   show j _ = j _, from congr_arg j $
-    (is_unit.coe_lift_right (f.to_map.mrestrict S) f.map_units _)⟩
+    (is_unit.coe_lift_right (f.to_map.restrict S) f.map_units _)⟩
 
 variables {g : M →* P}
 
@@ -646,7 +646,7 @@ lemma eq_of_eq (hg : ∀ y : S, is_unit (g y)) {x y} (h : f.to_map x = f.to_map
   g x = g y :=
 begin
   obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h,
-  rw [←mul_one (g x), ←is_unit.mul_lift_right_inv (g.mrestrict S) hg c],
+  rw [←mul_one (g x), ←is_unit.mul_lift_right_inv (g.restrict S) hg c],
   show _ * (g c * _) = _,
   rw [←mul_assoc, ←g.map_mul, hc, mul_inv_left hg, g.map_mul, mul_comm],
 end
@@ -673,7 +673,7 @@ of `add_comm_monoid`s `g : M →+ P` such that `g y` is invertible for all `y :
 induced from `N` to `P` sending `z : N` to `g x - g y`, where `(x, y) : M × S` are such that
 `z = f x - f y`."]
 noncomputable def lift : N →* P :=
-{ to_fun := λ z, g (f.sec z).1 * ↑(is_unit.lift_right (g.mrestrict S) hg (f.sec z).2)⁻¹,
+{ to_fun := λ z, g (f.sec z).1 * ↑(is_unit.lift_right (g.restrict S) hg (f.sec z).2)⁻¹,
   map_one' := by rw [mul_inv_left, mul_one]; exact f.eq_of_eq hg
     (by rw [←sec_spec, one_mul]),
   map_mul' := λ x y,
@@ -693,7 +693,7 @@ variables {S g}
 of `add_comm_monoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
 induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`."]
 lemma lift_mk' (x y) :
-  f.lift hg (f.mk' x y) = g x * ↑(is_unit.lift_right (g.mrestrict S) hg y)⁻¹ :=
+  f.lift hg (f.mk' x y) = g x * ↑(is_unit.lift_right (g.restrict S) hg y)⁻¹ :=
 (mul_inv hg).2 $ f.eq_of_eq hg $ by
   rw [f.to_map.map_mul, f.to_map.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]
 
@@ -818,7 +818,7 @@ begin
     obtain ⟨x, hx⟩ := f.surj z,
     use x,
     rw [←hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2)],
-    erw [is_unit.mul_lift_right_inv (g.mrestrict S) hg, mul_one] },
+    erw [is_unit.mul_lift_right_inv (g.restrict S) hg, mul_one] },
   { intros H v,
     obtain ⟨x, hx⟩ := H v,
     use f.mk' x.1 x.2,

src/group_theory/subgroup/basic.lean

@@ -2000,7 +2000,7 @@ homomorphism `G →* N`. -/
 @[to_additive "The canonical surjective `add_group` homomorphism `G →+ f(G)` induced by a group
 homomorphism `G →+ N`."]
 def range_restrict (f : G →* N) : G →* f.range :=
-monoid_hom.mk' (λ g, ⟨f g, ⟨g, rfl⟩⟩) $ λ a b, by {ext, exact f.map_mul' _ _}
+cod_restrict f _ $ λ x, ⟨x, rfl⟩
 
 @[simp, to_additive]
 lemma coe_range_restrict (f : G →* N) (g : G) : (f.range_restrict g : N) = f g := rfl
@@ -2031,27 +2031,6 @@ by { rw [range_eq_map, ← set_like.coe_set_eq, coe_map, subgroup.coe_subtype],
   (inclusion h_le).range = H.subgroup_of K :=
 subgroup.ext (λ g, set.ext_iff.mp (set.range_inclusion h_le) g)
 
-/-- Restriction of a group hom to a subgroup of the domain. -/
-@[to_additive "Restriction of an `add_group` hom to an `add_subgroup` of the domain."]
-def restrict (f : G →* N) (H : subgroup G) : H →* N :=
-f.comp H.subtype
-
-@[simp, to_additive]
-lemma restrict_apply {H : subgroup G} (f : G →* N) (x : H) :
-  f.restrict H x = f (x : G) := rfl
-
-/-- Restriction of a group hom to a subgroup of the codomain. -/
-@[to_additive "Restriction of an `add_group` hom to an `add_subgroup` of the codomain."]
-def cod_restrict (f : G →* N) (S : subgroup N) (h : ∀ x, f x ∈ S) : G →* S :=
-{ to_fun := λ n, ⟨f n, h n⟩,
-  map_one' := subtype.eq f.map_one,
-  map_mul' := λ x y, subtype.eq (f.map_mul x y) }
-
-@[simp, to_additive]
-lemma cod_restrict_apply {G : Type*} [group G] {N : Type*} [group N] (f : G →* N)
-  (S : subgroup N) (h : ∀ (x : G), f x ∈ S) {x : G} :
-    f.cod_restrict S h x = ⟨f x, h x⟩ := rfl
-
 @[to_additive] lemma subgroup_of_range_eq_of_le {G₁ G₂ : Type*} [group G₁] [group G₂]
   {K : subgroup G₂} (f : G₁ →* G₂) (h : f.range ≤ K) :
   f.range.subgroup_of K = (f.cod_restrict K (λ x, h ⟨x, rfl⟩)).range :=

src/group_theory/submonoid/operations.lean

@@ -52,8 +52,8 @@ In this file we define various operations on `submonoid`s and `monoid_hom`s.
 
 * `monoid_hom.mrange`: range of a monoid homomorphism as a submonoid of the codomain;
 * `monoid_hom.mker`: kernel of a monoid homomorphism as a submonoid of the domain;
-* `monoid_hom.mrestrict`: restrict a monoid homomorphism to a submonoid;
-* `monoid_hom.cod_mrestrict`: restrict the codomain of a monoid homomorphism to a submonoid;
+* `monoid_hom.restrict`: restrict a monoid homomorphism to a submonoid;
+* `monoid_hom.cod_restrict`: restrict the codomain of a monoid homomorphism to a submonoid;
 * `monoid_hom.mrange_restrict`: restrict a monoid homomorphism to its range;
 
 ## Tags
@@ -804,24 +804,28 @@ le_antisymm
 
 /-- Restriction of a monoid hom to a submonoid of the domain. -/
 @[to_additive "Restriction of an add_monoid hom to an `add_submonoid` of the domain."]
-def mrestrict {N : Type*} [mul_one_class N] (f : M →* N) (S : submonoid M) : S →* N :=
-f.comp S.subtype
+def restrict {N S : Type*} [mul_one_class N] [set_like S M] [submonoid_class S M]
+  (f : M →* N) (s : S) : s →* N :=
+f.comp (submonoid_class.subtype _)
 
 @[simp, to_additive]
-lemma mrestrict_apply {N : Type*} [mul_one_class N] (f : M →* N) (x : S) : f.mrestrict S x = f x :=
+lemma restrict_apply {N S : Type*} [mul_one_class N] [set_like S M] [submonoid_class S M]
+  (f : M →* N) (s : S) (x : s) : f.restrict s x = f x :=
 rfl
 
 /-- Restriction of a monoid hom to a submonoid of the codomain. -/
-@[to_additive "Restriction of an `add_monoid` hom to an `add_submonoid` of the codomain.", simps]
-def cod_mrestrict (f : M →* N) (S : submonoid N) (h : ∀ x, f x ∈ S) : M →* S :=
+@[to_additive "Restriction of an `add_monoid` hom to an `add_submonoid` of the codomain.",
+  simps apply]
+def cod_restrict {S} [set_like S N] [submonoid_class S N] (f : M →* N) (s : S)
+  (h : ∀ x, f x ∈ s) : M →* s :=
 { to_fun := λ n, ⟨f n, h n⟩,
   map_one' := subtype.eq f.map_one,
   map_mul' := λ x y, subtype.eq (f.map_mul x y) }
 
 /-- Restriction of a monoid hom to its range interpreted as a submonoid. -/
 @[to_additive "Restriction of an `add_monoid` hom to its range interpreted as a submonoid."]
 def mrange_restrict {N} [mul_one_class N] (f : M →* N) : M →* f.mrange :=
-f.cod_mrestrict f.mrange $ λ x, ⟨x, rfl⟩
+f.cod_restrict f.mrange $ λ x, ⟨x, rfl⟩
 
 @[simp, to_additive]
 lemma coe_mrange_restrict {N} [mul_one_class N] (f : M →* N) (x : M) :
@@ -951,7 +955,7 @@ by simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]
 /-- The monoid hom associated to an inclusion of submonoids. -/
 @[to_additive "The `add_monoid` hom associated to an inclusion of submonoids."]
 def inclusion {S T : submonoid M} (h : S ≤ T) : S →* T :=
-S.subtype.cod_mrestrict _ (λ x, h x.2)
+S.subtype.cod_restrict _ (λ x, h x.2)
 
 @[simp, to_additive]
 lemma range_subtype (s : submonoid M) : s.subtype.mrange = s :=

src/group_theory/subsemigroup/operations.lean

@@ -46,8 +46,8 @@ In this file we define various operations on `subsemigroup`s and `mul_hom`s.
 ### Operations on `mul_hom`s
 
 * `mul_hom.srange`: range of a semigroup homomorphism as a subsemigroup of the codomain;
-* `mul_hom.srestrict`: restrict a semigroup homomorphism to a subsemigroup;
-* `mul_hom.cod_srestrict`: restrict the codomain of a semigroup homomorphism to a subsemigroup;
+* `mul_hom.restrict`: restrict a semigroup homomorphism to a subsemigroup;
+* `mul_hom.cod_restrict`: restrict the codomain of a semigroup homomorphism to a subsemigroup;
 * `mul_hom.srange_restrict`: restrict a semigroup homomorphism to its range;
 
 ### Implementation notes
@@ -60,7 +60,7 @@ necessary.
 subsemigroup, range, product, map, comap
 -/
 
-variables {M N P : Type*}
+variables {M N P σ : Type*}
 
 /-!
 ### Conversion to/from `additive`/`multiplicative`
@@ -601,24 +601,27 @@ le_antisymm
 
 /-- Restriction of a semigroup hom to a subsemigroup of the domain. -/
 @[to_additive "Restriction of an add_semigroup hom to an `add_subsemigroup` of the domain."]
-def srestrict {N : Type*} [has_mul N] (f : M →ₙ* N) (S : subsemigroup M) : S →ₙ* N :=
+def restrict {N : Type*} [has_mul N] [set_like σ M] [mul_mem_class σ M] (f : M →ₙ* N) (S : σ) :
+  S →ₙ* N :=
 f.comp (mul_mem_class.subtype S)
 
 @[simp, to_additive]
-lemma srestrict_apply {N : Type*} [has_mul N] (f : M →ₙ* N) (x : S) : f.srestrict S x = f x :=
+lemma restrict_apply {N : Type*} [has_mul N] [set_like σ M] [mul_mem_class σ M] (f : M →ₙ* N)
+  {S : σ} (x : S) : f.restrict S x = f x :=
 rfl
 
 /-- Restriction of a semigroup hom to a subsemigroup of the codomain. -/
 @[to_additive "Restriction of an `add_semigroup` hom to an `add_subsemigroup` of the
 codomain.", simps]
-def cod_srestrict (f : M →ₙ* N) (S : subsemigroup N) (h : ∀ x, f x ∈ S) : M →ₙ* S :=
+def cod_restrict [set_like σ N] [mul_mem_class σ N] (f : M →ₙ* N) (S : σ) (h : ∀ x, f x ∈ S) :
+  M →ₙ* S :=
 { to_fun := λ n, ⟨f n, h n⟩,
   map_mul' := λ x y, subtype.eq (map_mul f x y) }
 
 /-- Restriction of a semigroup hom to its range interpreted as a subsemigroup. -/
 @[to_additive "Restriction of an `add_semigroup` hom to its range interpreted as a subsemigroup."]
 def srange_restrict {N} [has_mul N] (f : M →ₙ* N) : M →ₙ* f.srange :=
-f.cod_srestrict f.srange $ λ x, ⟨x, rfl⟩
+f.cod_restrict f.srange $ λ x, ⟨x, rfl⟩
 
 @[simp, to_additive]
 lemma coe_srange_restrict {N} [has_mul N] (f : M →ₙ* N) (x : M) :
@@ -680,7 +683,7 @@ by simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← srang
 /-- The semigroup hom associated to an inclusion of subsemigroups. -/
 @[to_additive "The `add_semigroup` hom associated to an inclusion of subsemigroups."]
 def inclusion {S T : subsemigroup M} (h : S ≤ T) : S →ₙ* T :=
-(mul_mem_class.subtype S).cod_srestrict _ (λ x, h x.2)
+(mul_mem_class.subtype S).cod_restrict _ (λ x, h x.2)
 
 @[simp, to_additive]
 lemma range_subtype (s : subsemigroup M) : (mul_mem_class.subtype s).srange = s :=

src/ring_theory/localization/basic.lean

@@ -390,13 +390,13 @@ begin
 end
 
 lemma mul_add_inv_left {g : R →+* P} (h : ∀ y : M, is_unit (g y)) (y : M) (w z₁ z₂ : P) :
-  w * ↑(is_unit.lift_right (g.to_monoid_hom.mrestrict M) h y)⁻¹ + z₁ = z₂
+  w * ↑(is_unit.lift_right (g.to_monoid_hom.restrict M) h y)⁻¹ + z₁ = z₂
     ↔ w + g y * z₁ = g y * z₂ :=
 begin
-  rw [mul_comm, ←one_mul z₁, ←units.inv_mul (is_unit.lift_right (g.to_monoid_hom.mrestrict M) h y),
+  rw [mul_comm, ←one_mul z₁, ←units.inv_mul (is_unit.lift_right (g.to_monoid_hom.restrict M) h y),
     mul_assoc, ←mul_add, units.inv_mul_eq_iff_eq_mul, units.inv_mul_cancel_left,
     is_unit.coe_lift_right],
-  simp only [ring_hom.to_monoid_hom_eq_coe, monoid_hom.mrestrict_apply, ring_hom.coe_monoid_hom]
+  simp only [ring_hom.to_monoid_hom_eq_coe, monoid_hom.restrict_apply, ring_hom.coe_monoid_hom]
 end
 
 lemma lift_spec_mul_add {g : R →+* P} (hg : ∀ y : M, is_unit (g y)) (z w w' v) :
@@ -435,7 +435,7 @@ variables {g : R →+* P} (hg : ∀ y : M, is_unit (g y))
 `g : R →* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
 `S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : R, y ∈ M`. -/
 lemma lift_mk' (x y) :
-  lift hg (mk' S x y) = g x * ↑(is_unit.lift_right (g.to_monoid_hom.mrestrict M) hg y)⁻¹ :=
+  lift hg (mk' S x y) = g x * ↑(is_unit.lift_right (g.to_monoid_hom.restrict M) hg y)⁻¹ :=
 (to_localization_map M S).lift_mk' _ _ _
 
 lemma lift_mk'_spec (x v) (y : M) :