diff --git a/src/algebra/category/Group/images.lean b/src/algebra/category/Group/images.lean
index 649e458a81b81..ab486f0bf88af 100644
--- a/src/algebra/category/Group/images.lean
+++ b/src/algebra/category/Group/images.lean
@@ -37,7 +37,7 @@ def image.ι : image f ⟶ H := f.range.subtype
 instance : mono (image.ι f) := concrete_category.mono_of_injective (image.ι f) subtype.val_injective
 
 /-- the corestriction map to the image -/
-def factor_thru_image : G ⟶ image f := f.to_range
+def factor_thru_image : G ⟶ image f := f.range_restrict
 
 lemma image.fac : factor_thru_image f ≫ image.ι f = f :=
 by { ext, refl, }
diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
index bbe8894fc7c70..a1f7104eed7a4 100644
--- a/src/group_theory/quotient_group.lean
+++ b/src/group_theory/quotient_group.lean
@@ -182,21 +182,21 @@ assume a b, quotient.induction_on₂' a b $
 show a⁻¹ * b ∈ ker φ, by rw [mem_ker,
   is_mul_hom.map_mul φ, ← h, is_group_hom.map_inv φ, inv_mul_self]
 
--- Note that ker φ isn't definitionally ker (to_range φ)
+-- Note that `ker φ` isn't definitionally `ker (φ.range_restrict)`
 -- so there is a bit of annoying code duplication here
 
 /-- The induced map from the quotient by the kernel to the range. -/
 @[to_additive quotient_add_group.range_ker_lift "The induced map from the quotient by the kernel to
 the range."]
 def range_ker_lift : quotient (ker φ) →* φ.range :=
-lift _ (to_range φ) $ λ g hg, (mem_ker _).mp $ by rwa to_range_ker
+lift _ φ.range_restrict $ λ g hg, (mem_ker _).mp $ by rwa range_restrict_ker
 
 @[to_additive quotient_add_group.range_ker_lift_injective]
 lemma range_ker_lift_injective : injective (range_ker_lift φ) :=
 assume a b, quotient.induction_on₂' a b $
-  assume a b (h : to_range φ a = to_range φ b), quotient.sound' $
-show a⁻¹ * b ∈ ker φ, by rw [←to_range_ker, mem_ker,
-  is_mul_hom.map_mul (to_range φ), ← h, is_group_hom.map_inv (to_range φ), inv_mul_self]
+  assume a b (h : φ.range_restrict a = φ.range_restrict b), quotient.sound' $
+show a⁻¹ * b ∈ ker φ, by rw [←range_restrict_ker, mem_ker,
+  φ.range_restrict.map_mul, ← h, φ.range_restrict.map_inv, inv_mul_self]
 
 @[to_additive quotient_add_group.range_ker_lift_surjective]
 lemma range_ker_lift_surjective : surjective (range_ker_lift φ) :=
diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean
index 0813e92138f19..48be104d78523 100644
--- a/src/group_theory/subgroup.lean
+++ b/src/group_theory/subgroup.lean
@@ -1096,9 +1096,12 @@ by ext; simp
 homomorphism `G →* N`. -/
 @[to_additive "The canonical surjective `add_group` homomorphism `G →+ f(G)` induced by a group
 homomorphism `G →+ N`."]
-def to_range (f : G →* N) : G →* f.range :=
+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' _ _}
 
+@[simp, to_additive]
+lemma coe_range_restrict (f : G →* N) (g : G) : (f.range_restrict g : N) = f g := rfl
+
 @[to_additive]
 lemma map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range :=
 by rw [range_eq_map, range_eq_map]; exact (⊤ : subgroup G).map_map g f
@@ -1147,7 +1150,7 @@ instance decidable_mem_ker [decidable_eq N] (f : G →* N) :
 @[to_additive]
 lemma comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker := rfl
 
-@[to_additive] lemma to_range_ker (f : G →* N) : ker (to_range f) = ker f :=
+@[to_additive] lemma range_restrict_ker (f : G →* N) : ker (range_restrict f) = ker f :=
 begin
   ext,
   change (⟨f x, _⟩ : range f) = ⟨1, _⟩ ↔ f x = 1,