refactor(group_theory/submonoid): adjust definitional unfolding of ad…

…d_monoid_hom.mrange to match set.range (#7227)

This changes the following to unfold to `set.range`:

* `monoid_hom.mrange`
* `add_monoid_hom.mrange`
* `linear_map.range`
* `lie_hom.range`
* `ring_hom.range`
* `ring_hom.srange`
* `ring_hom.field_range`
* `alg_hom.range`

For example:
```lean
import ring_theory.subring

variables (R : Type*) [ring R] (f : R →+* R)

-- before this PR, these required `f '' univ` on the RHS
example : (f.range : set R) = set.range f := rfl
example : (f.srange : set R) = set.range f := rfl
example : (f.to_monoid_hom.mrange : set R) = set.range f := rfl

-- this one is unchanged by this PR
example : (f.to_add_monoid_hom.range : set R) = set.range f := rfl
```

The motivations behind this change are that
* It eliminates a lot of `∈ set.univ` hypotheses and goals that are just annoying
* it means that an equivalence like `A ≃ set.range f` is defeq to `A ≃ f.range`, with no need to insert awkward `equiv.cast`-like terms to translate between different approaches
* `monoid_hom.range` (as opposed to `mrange`) already used this pattern.

The number of lines has gone up a bit, but most of those are comments explaining the design choice.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60set.2Erange.20f.60.20vs.20.60f.20''.20univ.60/near/234893679)

src/algebra/algebra/subalgebra.lean

@@ -56,7 +56,7 @@ theorem algebra_map_mem (r : R) : algebra_map R A r ∈ S :=
 S.algebra_map_mem' r
 
 theorem srange_le : (algebra_map R A).srange ≤ S.to_subsemiring :=
-λ x ⟨r, _, hr⟩, hr ▸ S.algebra_map_mem r
+λ x ⟨r, hr⟩, hr ▸ S.algebra_map_mem r
 
 theorem range_subset : set.range (algebra_map R A) ⊆ S :=
 λ x ⟨r, hr⟩, hr ▸ S.algebra_map_mem r
@@ -349,7 +349,7 @@ variables (φ : A →ₐ[R] B)
 
 /-- Range of an `alg_hom` as a subalgebra. -/
 protected def range (φ : A →ₐ[R] B) : subalgebra R B :=
-{ algebra_map_mem' := λ r, ⟨algebra_map R A r, set.mem_univ _, φ.commutes r⟩,
+{ algebra_map_mem' := λ r, ⟨algebra_map R A r, φ.commutes r⟩,
   .. φ.to_ring_hom.srange }
 
 @[simp] lemma mem_range (φ : A →ₐ[R] B) {y : B} :
@@ -497,7 +497,7 @@ theorem eq_top_iff {S : subalgebra R A} :
 
 @[simp] theorem map_top (f : A →ₐ[R] B) : subalgebra.map (⊤ : subalgebra R A) f = f.range :=
 subalgebra.ext $ λ x,
-  ⟨λ ⟨y, _, hy⟩, ⟨y, set.mem_univ _, hy⟩, λ ⟨y, mem, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩
+  ⟨λ ⟨y, _, hy⟩, ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨y, algebra.mem_top, hy⟩⟩
 
 @[simp] theorem map_bot (f : A →ₐ[R] B) : subalgebra.map (⊥ : subalgebra R A) f = ⊥ :=
 eq_bot_iff.2 $ λ x ⟨y, hy, hfy⟩, let ⟨r, hr⟩ := mem_bot.1 hy in subalgebra.range_le _

src/algebra/algebra/tower.lean

@@ -262,8 +262,7 @@ show z ∈ subsemiring.closure (set.range (algebra_map (to_alg_hom R S A).range
   z ∈ subsemiring.closure (set.range (algebra_map S A) ∪ t : set A),
 from suffices set.range (algebra_map (to_alg_hom R S A).range A) = set.range (algebra_map S A),
   by rw this,
-by { ext z, exact ⟨λ ⟨⟨x, y, _, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩,
-  ⟨⟨z, y, set.mem_univ _, hy⟩, rfl⟩⟩ }
+by { ext z, exact ⟨λ ⟨⟨x, y, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y, hy⟩, ⟨⟨z, y, hy⟩, rfl⟩⟩ }
 
 end is_scalar_tower
 

src/algebra/lie/nilpotent.lean

@@ -110,7 +110,9 @@ lemma lie_ideal.lower_central_series_map_eq (k : ℕ) {f : L →ₗ⁅R⁆ L'}
   (h : function.surjective f) :
   lie_ideal.map f (lower_central_series R L L k) = lower_central_series R L' L' k :=
 begin
-  have h' : (⊤ : lie_ideal R L).map f = ⊤, { exact f.ideal_range_eq_top_of_surjective h, },
+  have h' : (⊤ : lie_ideal R L).map f = ⊤,
+  { rw ←f.ideal_range_eq_map,
+    exact f.ideal_range_eq_top_of_surjective h, },
   induction k with k ih,
   { simp only [lie_module.lower_central_series_zero], exact h', },
   { simp only [lie_module.lower_central_series_succ, lie_ideal.map_bracket_eq f h, ih, h'], },

src/algebra/lie/solvable.lean

@@ -171,9 +171,10 @@ end
 lemma derived_series_map_eq (k : ℕ) (h : function.surjective f) :
   (derived_series R L' k).map f = derived_series R L k :=
 begin
-  have h' : (⊤ : lie_ideal R L').map f = ⊤, { exact f.ideal_range_eq_top_of_surjective h, },
   induction k with k ih,
-  { exact h', },
+  { change (⊤ : lie_ideal R L').map f = ⊤,
+    rw ←f.ideal_range_eq_map,
+    exact f.ideal_range_eq_top_of_surjective h, },
   { simp only [derived_series_def, map_bracket_eq f h, ih, derived_series_of_ideal_succ], },
 end
 

src/algebra/lie/subalgebra.lean

@@ -259,6 +259,9 @@ instance : has_top (lie_subalgebra R L) :=
 
 @[simp] lemma mem_top (x : L) : x ∈ (⊤ : lie_subalgebra R L) := mem_univ x
 
+lemma _root_.lie_hom.range_eq_map : f.range = map f ⊤ :=
+by { ext, simp }
+
 instance : has_inf (lie_subalgebra R L) :=
 ⟨λ K K', { lie_mem' := λ x y hx hy, mem_inter (K.lie_mem hx.1 hy.1) (K'.lie_mem hx.2 hy.2),
             ..(K ⊓ K' : submodule R L) }⟩

src/algebra/lie/submodule.lean

@@ -506,11 +506,15 @@ variables (f : L →ₗ⁅R⁆ L') (I : lie_ideal R L) (J : lie_ideal R L')
 def ker : lie_ideal R L := lie_ideal.comap f ⊥
 
 /-- The range of a morphism of Lie algebras as an ideal in the codomain. -/
-def ideal_range : lie_ideal R L' := lie_ideal.map f ⊤
+def ideal_range : lie_ideal R L' := lie_submodule.lie_span R L' f.range
 
 lemma ideal_range_eq_lie_span_range :
   f.ideal_range = lie_submodule.lie_span R L' f.range := rfl
 
+lemma ideal_range_eq_map :
+  f.ideal_range = lie_ideal.map f ⊤ :=
+by { ext, simp only [ideal_range, range_eq_map], refl }
+
 /-- The condition that the image of a morphism of Lie algebras is an ideal. -/
 def is_ideal_morphism : Prop := (f.ideal_range : lie_subalgebra R L') = f.range
 
@@ -532,7 +536,11 @@ end
 
 lemma range_subset_ideal_range : (f.range : set L') ⊆ f.ideal_range := lie_submodule.subset_lie_span
 
-lemma map_le_ideal_range : I.map f ≤ f.ideal_range := lie_ideal.map_mono le_top
+lemma map_le_ideal_range : I.map f ≤ f.ideal_range :=
+begin
+  rw f.ideal_range_eq_map,
+  exact lie_ideal.map_mono le_top,
+end
 
 lemma ker_le_comap : f.ker ≤ J.comap f := lie_ideal.comap_mono bot_le
 
@@ -542,7 +550,11 @@ lemma ker_le_comap : f.ker ≤ J.comap f := lie_ideal.comap_mono bot_le
 show x ∈ (f.ker : submodule R L) ↔ _,
 by simp only [ker_coe_submodule, linear_map.mem_ker, coe_to_linear_map]
 
-lemma mem_ideal_range {x : L} : f x ∈ ideal_range f := lie_ideal.mem_map (lie_submodule.mem_top x)
+lemma mem_ideal_range {x : L} : f x ∈ ideal_range f :=
+begin
+  rw ideal_range_eq_map,
+  exact lie_ideal.mem_map (lie_submodule.mem_top x)
+end
 
 @[simp] lemma mem_ideal_range_iff (h : is_ideal_morphism f) {y : L'} :
   y ∈ ideal_range f ↔ ∃ (x : L), f x = y :=
@@ -663,7 +675,7 @@ begin
   { rw le_inf_iff, exact ⟨f.map_le_ideal_range _, map_comap_le⟩, },
   { rw f.is_ideal_morphism_def at h,
     rw [lie_submodule.le_def, lie_submodule.inf_coe, ← coe_to_subalgebra, h],
-    rintros y ⟨⟨x, h₁, h₂⟩, h₃⟩, rw ← h₂ at h₃ ⊢, exact mem_map h₃, },
+    rintros y ⟨⟨x, h₁⟩, h₂⟩, rw ← h₁ at h₂ ⊢, exact mem_map h₂, },
 end
 
 @[simp] lemma comap_map_eq (h : ↑(map f I) = f '' I) : comap f (map f I) = I ⊔ f.ker :=

src/field_theory/adjoin.lean

@@ -434,12 +434,11 @@ alg_equiv.of_bijective (alg_hom.mk (adjoin_root.lift (algebra_map F F⟮α⟯)
     split,
     { exact ring_hom.injective f },
     { suffices : F⟮α⟯.to_subfield ≤ ring_hom.field_range ((F⟮α⟯.to_subfield.subtype).comp f),
-      { exact λ x, Exists.cases_on (this (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy.2⟩) },
-      exact subfield.closure_le.mpr (set.union_subset (λ x hx, Exists.cases_on hx (λ y hy, ⟨y,
-        ⟨subfield.mem_top y, by { rw [ring_hom.comp_apply, adjoin_root.lift_of], exact hy }⟩⟩))
+      { exact λ x, Exists.cases_on (this (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy⟩) },
+      exact subfield.closure_le.mpr (set.union_subset (λ x hx, Exists.cases_on hx (λ y hy,
+        ⟨y, by { rw [ring_hom.comp_apply, adjoin_root.lift_of], exact hy }⟩))
         (set.singleton_subset_iff.mpr ⟨adjoin_root.root (minpoly F α),
-        ⟨subfield.mem_top (adjoin_root.root (minpoly F α)),
-        by { rw [ring_hom.comp_apply, adjoin_root.lift_root], refl }⟩⟩)) } end)
+        by { rw [ring_hom.comp_apply, adjoin_root.lift_root], refl }⟩)) } end)
 
 lemma adjoin_root_equiv_adjoin_apply_root (h : is_integral F α) :
   adjoin_root_equiv_adjoin F h (adjoin_root.root (minpoly F α)) =

src/field_theory/minpoly.lean

@@ -74,7 +74,7 @@ begin
   have key := minpoly.aeval A x,
   rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leading_coeff, C_1, one_mul, aeval_add,
       aeval_C, aeval_X, ←eq_neg_iff_add_eq_zero, ←ring_hom.map_neg] at key,
-  exact ⟨-(minpoly A x).coeff 0, subring.mem_top (-(minpoly A x).coeff 0), key.symm⟩,
+  exact ⟨-(minpoly A x).coeff 0, key.symm⟩,
 end
 
 /--The defining property of the minimal polynomial of an element x:

src/field_theory/normal.lean

@@ -99,7 +99,7 @@ lemma alg_hom.normal_bijective [h : normal F E] (ϕ : E →ₐ[F] K) : function.
     { rw [ring_hom.map_zero, aeval_map, ←is_scalar_tower.to_alg_hom_apply F K E,
           ←alg_hom.comp_apply, ←aeval_alg_hom],
       exact minpoly.aeval F (algebra_map K E x) })))) with y hy,
-  exact ⟨y, hy.2⟩ }⟩
+  exact ⟨y, hy⟩ }⟩
 
 variables {F} {E} {E' : Type*} [field E'] [algebra F E']
 
@@ -200,7 +200,7 @@ def alg_hom.restrict_normal_aux [h : normal F E] :
 { to_fun := λ x, ⟨ϕ x, by
   { suffices : (to_alg_hom F E K).range.map ϕ ≤ _,
     { exact this ⟨x, subtype.mem x, rfl⟩ },
-    rintros x ⟨y, ⟨z, -, hy⟩, hx⟩,
+    rintros x ⟨y, ⟨z, hy⟩, hx⟩,
     rw [←hx, ←hy],
     apply minpoly.mem_range_of_degree_eq_one E,
     exact or.resolve_left (h.splits z) (minpoly.ne_zero (h.is_integral z))
@@ -224,7 +224,7 @@ def alg_hom.restrict_normal [normal F E] : E →ₐ[F] E :=
   algebra_map E K (ϕ.restrict_normal E x) = ϕ (algebra_map E K x) :=
 subtype.ext_iff.mp (alg_equiv.apply_symm_apply (alg_equiv.of_injective_field
   (is_scalar_tower.to_alg_hom F E K)) (ϕ.restrict_normal_aux E
-    ⟨is_scalar_tower.to_alg_hom F E K x, ⟨x, ⟨subsemiring.mem_top x, rfl⟩⟩⟩))
+    ⟨is_scalar_tower.to_alg_hom F E K x, x, rfl⟩))
 
 lemma alg_hom.restrict_normal_comp [normal F E] :
   (ϕ.restrict_normal E).comp (ψ.restrict_normal E) = (ϕ.comp ψ).restrict_normal E :=

src/field_theory/splitting_field.lean

@@ -447,7 +447,7 @@ alg_equiv.symm $ alg_equiv.of_bijective
     adjoin_root.induction_on _ p $ λ p hp, ideal.quotient.eq_zero_iff_mem.2 $
     ideal.mem_span_singleton.2 $ minpoly.dvd F x hp,
   λ y,
-    let ⟨p, _, hp⟩ := (set_like.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) (y : R)).1 y.2 in
+    let ⟨p, hp⟩ := (set_like.ext_iff.1 (algebra.adjoin_singleton_eq_range F x) (y : R)).1 y.2 in
     ⟨adjoin_root.mk _ p, subtype.eq hp⟩⟩
 
 open finset

src/field_theory/subfield.lean

@@ -287,15 +287,21 @@ variables (g : L →+* M) (f : K →+* L)
 /-! # range -/
 
 /-- The range of a ring homomorphism, as a subfield of the target. -/
-def field_range : subfield L := (⊤ : subfield K).map f
+def field_range : subfield L :=
+((⊤ : subfield K).map f).copy (set.range f) set.image_univ.symm
 
-@[simp] lemma coe_field_range : (f.field_range : set L) = set.range f := set.image_univ
+/-- Note that `ring_hom.field_range` is deliberately defined in a way that makes this true by `rfl`,
+as this means the types `↥(set.range f)` and `↥f.field_range` are interchangeable without proof
+obligations. -/
+@[simp] lemma coe_field_range : (f.field_range : set L) = set.range f := rfl
 
-@[simp] lemma mem_field_range {f : K →+* L} {y : L} : y ∈ f.range ↔ ∃ x, f x = y :=
-by simp [range]
+@[simp] lemma mem_field_range {f : K →+* L} {y : L} : y ∈ f.field_range ↔ ∃ x, f x = y := iff.rfl
+
+lemma field_range_eq_map : f.field_range = subfield.map f ⊤ :=
+by { ext, simp }
 
 lemma map_field_range : f.field_range.map g = (g.comp f).field_range :=
-(⊤ : subfield K).map_map g f
+by simpa only [field_range_eq_map] using (⊤ : subfield K).map_map g f
 
 end ring_hom
 
@@ -549,8 +555,8 @@ def restrict_field (f : K →+* L) (s : subfield K) : s →+* L := f.comp s.subt
 @[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.range :=
-f.cod_restrict' f.range $ λ x, ⟨x, subfield.mem_top x, rfl⟩
+def range_restrict_field (f : K →+* L) : K →+* f.field_range :=
+f.srange_restrict
 
 @[simp] lemma coe_range_restrict_field (f : K →+* L) (x : K) :
   (f.range_restrict_field x : L) = f x := rfl

src/group_theory/congruence.lean

@@ -727,10 +727,7 @@ lift_funext g (c.lift f H) $ λ x, by rw [lift_coe H, ←comp_mk'_apply, Hg]
 constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces
 on the quotient."]
 theorem lift_range (H : c ≤ ker f) : (c.lift f H).mrange = f.mrange :=
-submonoid.ext $ λ x,
-  ⟨λ ⟨y, hy⟩, by revert hy; rcases y; exact
-     λ hy, ⟨y, hy.1, by rw [hy.2.symm, ←lift_coe H]; refl⟩,
-   λ ⟨y, hy⟩, ⟨↑y, hy.1, by rw ←hy.2; refl⟩⟩
+submonoid.ext $ λ x, ⟨by rintros ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩, λ ⟨y, hy⟩, ⟨↑y, hy⟩⟩
 
 /-- Surjective monoid homomorphisms constant on a congruence relation `c`'s equivalence classes
     induce a surjective homomorphism on `c`'s quotient. -/
@@ -810,7 +807,7 @@ noncomputable def quotient_ker_equiv_range (f : M →* P) : (ker f).quotient ≃
         $ mul_equiv.submonoid_congr ker_lift_range_eq).comp (ker_lift f).mrange_restrict) $
       (equiv.bijective _).comp
         ⟨λ x y h, ker_lift_injective f $ by rcases x; rcases y; injections,
-         λ ⟨w, z, hzm, hz⟩, ⟨z, by rcases hz; rcases _x; refl⟩⟩ }
+         λ ⟨w, z, hz⟩, ⟨z, by rcases hz; rcases _x; refl⟩⟩ }
 
 /-- The first isomorphism theorem for monoids in the case of a surjective homomorphism. -/
 @[to_additive "The first isomorphism theorem for `add_monoid`s in the case of a surjective

src/group_theory/submonoid/membership.lean

@@ -170,8 +170,8 @@ variables [monoid M]
 open monoid_hom
 
 lemma closure_singleton_eq (x : M) : closure ({x} : set M) = (powers_hom M x).mrange :=
-closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, trivial, pow_one x⟩) $
-  λ x ⟨n, _, hn⟩, hn ▸ pow_mem _ (subset_closure $ set.mem_singleton _) _
+closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, pow_one x⟩) $
+  λ x ⟨n, hn⟩, hn ▸ pow_mem _ (subset_closure $ set.mem_singleton _) _
 
 /-- The submonoid generated by an element of a monoid equals the set of natural number powers of
     the element. -/
@@ -186,7 +186,7 @@ by simp [eq_bot_iff_forall, mem_closure_singleton]
 
 @[to_additive]
 lemma closure_eq_mrange (s : set M) : closure s = (free_monoid.lift (coe : s → M)).mrange :=
-by rw [mrange, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp,
+by rw [mrange_eq_map, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp,
   free_monoid.lift_comp_of, subtype.range_coe]
 
 @[to_additive]
@@ -221,7 +221,7 @@ open monoid_hom
 
 @[to_additive]
 lemma sup_eq_range (s t : submonoid N) : s ⊔ t = (s.subtype.coprod t.subtype).mrange :=
-by rw [mrange, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl,
+by rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl,
   map_mrange, coprod_comp_inr, range_subtype, range_subtype]
 
 @[to_additive]
@@ -244,8 +244,8 @@ lemma nsmul_mem (S : add_submonoid A) {x : A} (hx : x ∈ S) :
 | (n+1) := by { rw [add_nsmul, one_nsmul], exact S.add_mem (nsmul_mem n) hx }
 
 lemma closure_singleton_eq (x : A) : closure ({x} : set A) = (multiples_hom A x).mrange :=
-closure_eq_of_le (set.singleton_subset_iff.2 ⟨1, trivial, one_nsmul x⟩) $
-  λ x ⟨n, _, hn⟩, hn ▸ nsmul_mem _ (subset_closure $ set.mem_singleton _) _
+closure_eq_of_le (set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) $
+  λ x ⟨n, hn⟩, hn ▸ nsmul_mem _ (subset_closure $ set.mem_singleton _) _
 
 /-- The `add_submonoid` generated by an element of an `add_monoid` equals the set of
 natural number multiples of the element. -/

src/group_theory/submonoid/operations.lean

@@ -546,19 +546,32 @@ open submonoid
 
 /-- The range of a monoid homomorphism is a submonoid. -/
 @[to_additive "The range of an `add_monoid_hom` is an `add_submonoid`."]
-def mrange (f : M →* N) : submonoid N := (⊤ : submonoid M).map f
+def mrange (f : M →* N) : submonoid N :=
+((⊤ : submonoid M).map f).copy (set.range f) set.image_univ.symm
 
-@[simp, to_additive] lemma coe_mrange (f : M →* N) :
+/-- Note that `monoid_hom.mrange` is deliberately defined in a way that makes this true by `rfl`,
+as this means the types `↥(set.range f)` and `↥f.mrange` are interchangeable without proof
+obligations. -/
+@[simp, to_additive]
+lemma coe_mrange (f : M →* N) :
   (f.mrange : set N) = set.range f :=
-set.image_univ
+rfl
+
+/-- Note that `add_monoid_hom.mrange` is deliberately defined in a way that makes this true by
+`rfl`, as this means the types `↥(set.range f)` and `↥f.mrange` are interchangeable without proof
+obligations. -/
+add_decl_doc add_monoid_hom.coe_mrange
 
 @[simp, to_additive] lemma mem_mrange {f : M →* N} {y : N} :
   y ∈ f.mrange ↔ ∃ x, f x = y :=
-by simp [mrange]
+iff.rfl
+
+@[to_additive] lemma mrange_eq_map (f : M →* N) : f.mrange = (⊤ : submonoid M).map f :=
+by ext; simp
 
 @[to_additive]
 lemma map_mrange (g : N →* P) (f : M →* N) : f.mrange.map g = (g.comp f).mrange :=
-(⊤ : submonoid M).map_map g f
+by simpa only [mrange_eq_map] using (⊤ : submonoid M).map_map g f
 
 @[to_additive]
 lemma mrange_top_iff_surjective {N} [mul_one_class N] {f : M →* N} :
@@ -571,9 +584,6 @@ lemma mrange_top_of_surjective {N} [mul_one_class N] (f : M →* N) (hf : functi
   f.mrange = (⊤ : submonoid N) :=
 mrange_top_iff_surjective.2 hf
 
-@[to_additive]
-lemma mrange_eq_map (f : M →* N) : f.mrange = map f ⊤ := rfl
-
 @[to_additive]
 lemma mclosure_preimage_le (f : M →* N) (s : set N) :
   closure (f ⁻¹' s) ≤ (closure s).comap f :=
@@ -609,7 +619,7 @@ def cod_mrestrict (f : M →* N) (S : submonoid N) (h : ∀ x, f x ∈ S) : M 
 /-- 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, submonoid.mem_top x, rfl⟩
+f.cod_mrestrict f.mrange $ λ x, ⟨x, rfl⟩
 
 @[simp, to_additive]
 lemma coe_mrange_restrict {N} [mul_one_class N] (f : M →* N) (x : M) :
@@ -622,10 +632,12 @@ namespace submonoid
 open monoid_hom
 
 @[to_additive]
-lemma mrange_inl : (inl M N).mrange = prod ⊤ ⊥ := map_inl ⊤
+lemma mrange_inl : (inl M N).mrange = prod ⊤ ⊥ :=
+by simpa only [mrange_eq_map] using map_inl ⊤
 
 @[to_additive]
-lemma mrange_inr : (inr M N).mrange = prod ⊥ ⊤ := map_inr ⊤
+lemma mrange_inr : (inr M N).mrange = prod ⊥ ⊤ :=
+by simpa only [mrange_eq_map] using map_inr ⊤
 
 @[to_additive]
 lemma mrange_inl' : (inl M N).mrange = comap (snd M N) ⊥ := mrange_inl.trans (top_prod _)