feat(algebra/lie/tensor_product): prove lie_submodule.lie_ideal_oper_eq_tensor_map_range (#7313)

The lemma `coe_lift_lie_eq_lift_coe` also introduced here is an unrelated change but is a stronger form of `lift_lie_apply` that is worth having.

See also this [Zulip remark](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60linear_map.2Erange_eq_map.60.20vs.20.60submodule.2Emap_top.60/near/235845192) concerning the proposed library note.

Author: ocfnash

src/algebra/lie/abelian.lean

@@ -199,12 +199,17 @@ def maximal_trivial_linear_map_equiv_lie_module_hom :
   ((maximal_trivial_linear_map_equiv_lie_module_hom f) : M → N) = f :=
 by { ext, refl, }
 
-@[simp] lemma coe_maximal_trivial_linear_map_equiv_lie_module_hom_apply
+@[simp] lemma coe_maximal_trivial_linear_map_equiv_lie_module_hom_symm
+  (f : M →ₗ⁅R,L⁆ N) :
+  ((maximal_trivial_linear_map_equiv_lie_module_hom.symm f) : M → N) = f :=
+rfl
+
+@[simp] lemma coe_linear_map_maximal_trivial_linear_map_equiv_lie_module_hom
   (f : maximal_trivial_submodule R L (M →ₗ[R] N)) :
   ((maximal_trivial_linear_map_equiv_lie_module_hom f) : M →ₗ[R] N) = (f : M →ₗ[R] N) :=
 by { ext, refl, }
 
-@[simp] lemma coe_maximal_trivial_linear_map_equiv_lie_module_hom_symm_apply
+@[simp] lemma coe_linear_map_maximal_trivial_linear_map_equiv_lie_module_hom_symm
   (f : M →ₗ⁅R,L⁆ N) :
   ((maximal_trivial_linear_map_equiv_lie_module_hom.symm f) : M →ₗ[R] N) = (f : M →ₗ[R] N) :=
 rfl

src/algebra/lie/basic.lean

@@ -253,12 +253,18 @@ def comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →
 { map_lie' := λ x y, by { change f (g ⁅x, y⁆) = ⁅f (g x), f (g y)⁆, rw [map_lie, map_lie], },
   ..linear_map.comp f.to_linear_map g.to_linear_map }
 
-@[simp] lemma comp_apply (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :
+lemma comp_apply (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :
   f.comp g x = f (g x) := rfl
 
-@[norm_cast]
-lemma comp_coe (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
-  (f : L₂ → L₃) ∘ (g : L₁ → L₂) = f.comp g := rfl
+@[norm_cast, simp]
+lemma coe_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
+  (f.comp g : L₁ → L₃) = f ∘ g :=
+rfl
+
+@[norm_cast, simp]
+lemma coe_linear_map_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
+  (f.comp g : L₁ →ₗ[R] L₃) = (f : L₂ →ₗ[R] L₃).comp (g : L₁ →ₗ[R] L₂) :=
+rfl
 
 /-- The inverse of a bijective morphism is a morphism. -/
 def inverse (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁)
@@ -445,11 +451,16 @@ def comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆
 { map_lie' := λ x m, by { change f (g ⁅x, m⁆) = ⁅x, f (g m)⁆, rw [map_lie, map_lie], },
   ..linear_map.comp f.to_linear_map g.to_linear_map }
 
-@[simp] lemma comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) :
+lemma comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) :
   f.comp g m = f (g m) := rfl
 
-@[norm_cast] lemma comp_coe (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
-  (f : N → P) ∘ (g : M → N) = f.comp g := rfl
+@[norm_cast, simp] lemma coe_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
+  (f.comp g : M → P) = f ∘ g :=
+rfl
+
+@[norm_cast, simp] lemma coe_linear_map_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
+  (f.comp g : M →ₗ[R] P) = (f : N →ₗ[R] P).comp (g : M →ₗ[R] N) :=
+rfl
 
 /-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules. -/
 def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M)

src/algebra/lie/ideal_operations.lean

@@ -50,6 +50,7 @@ instance has_bracket : has_bracket (lie_ideal R L) (lie_submodule R L M) :=
 lemma lie_ideal_oper_eq_span :
   ⁅I, N⁆ = lie_span R L { m | ∃ (x : I) (n : N), ⁅(x : L), (n : M)⁆ = m } := rfl
 
+/-- See also `lie_submodule.lie_ideal_oper_eq_tensor_map_range`. -/
 lemma lie_ideal_oper_eq_linear_span :
   (↑⁅I, N⁆ : submodule R M) = submodule.span R { m | ∃ (x : I) (n : N), ⁅(x : L), (n : M)⁆ = m } :=
 begin

src/algebra/lie/of_associative.lean

@@ -103,7 +103,9 @@ variables (R : Type u) (L : Type v) (M : Type w)
 variables [comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
 variables [lie_ring_module L M] [lie_module R L M]
 
-/-- A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module. -/
+/-- A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module.
+
+See also `lie_module.to_module_hom`. -/
 @[simps] def lie_module.to_endomorphism : L →ₗ⁅R⁆ module.End R M :=
 { to_fun    := λ x,
   { to_fun    := λ m, ⁅x, m⁆,

src/algebra/lie/submodule.lean

@@ -89,6 +89,15 @@ begin
   { rw h, },
 end
 
+/-- Copy of a lie_submodule with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+protected def copy (s : set M) (hs : s = ↑N) : lie_submodule R L M :=
+{ carrier := s,
+  zero_mem' := hs.symm ▸ N.zero_mem',
+  add_mem'  := hs.symm ▸ N.add_mem',
+  smul_mem' := hs.symm ▸ N.smul_mem',
+  lie_mem   := hs.symm ▸ N.lie_mem, }
+
 instance : lie_ring_module L N :=
 { bracket     := λ (x : L) (m : N), ⟨⁅x, m.val⁆, N.lie_mem m.property⟩,
   add_lie     := by { intros x y m, apply set_coe.ext, apply add_lie, },
@@ -416,6 +425,10 @@ lemma map_le_iff_le_comap {f : M →ₗ⁅R,L⁆ M'} {N : lie_submodule R L M} {
 lemma gc_map_comap (f : M →ₗ⁅R,L⁆ M') : galois_connection (map f) (comap f) :=
 λ N N', map_le_iff_le_comap
 
+@[simp] lemma mem_map (f : M →ₗ⁅R,L⁆ M') (N : lie_submodule R L M) (m' : M') :
+  m' ∈ N.map f ↔ ∃ m, m ∈ N ∧ f m = m' :=
+submodule.mem_map
+
 end lie_submodule
 
 namespace lie_ideal
@@ -719,6 +732,31 @@ end lie_ideal
 
 end lie_submodule_map_and_comap
 
+namespace lie_module_hom
+
+variables {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
+variables [comm_ring R] [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
+variables [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N]
+variables (f : M →ₗ⁅R,L⁆ N)
+
+/-- The range of a morphism of Lie modules `f : M → N` is a Lie submodule of `N`.
+See Note [range copy pattern]. -/
+def range : lie_submodule R L N :=
+(lie_submodule.map f ⊤).copy (set.range f) set.image_univ.symm
+
+@[simp] lemma coe_range : (f.range : set N) = set.range f := rfl
+
+@[simp] lemma coe_submodule_range : (f.range : submodule R N) = (f : M →ₗ[R] N).range := rfl
+
+@[simp] lemma mem_range (n : N) : n ∈ f.range ↔ ∃ m, f m = n :=
+iff.rfl
+
+lemma map_top : lie_submodule.map f ⊤ = f.range :=
+by { ext, simp, }
+
+end lie_module_hom
+
 section top_equiv_self
 
 variables {R : Type u} {L : Type v}

src/algebra/lie/tensor_product.lean

@@ -15,23 +15,24 @@ Tensor products of Lie modules carry natural Lie module structures.
 lie module, tensor product, universal property
 -/
 
-universes u v w w₁ w₂
+universes u v w w₁ w₂ w₃
+
+variables {R : Type u} [comm_ring R]
 
 namespace tensor_product
 
 open_locale tensor_product
 
-variables {R : Type u} [comm_ring R]
-
 namespace lie_module
 
 open lie_module
 
-variables {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂}
+variables {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃}
 variables [lie_ring L] [lie_algebra R L]
 variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
 variables [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N]
 variables [add_comm_group P] [module R P] [lie_ring_module L P] [lie_module R L P]
+variables [add_comm_group Q] [module R Q] [lie_ring_module L Q] [lie_module R L Q]
 
 /-- It is useful to define the bracket via this auxiliary function so that we have a type-theoretic
 expression of the fact that `L` acts by linear endomorphisms. It simplifies the proofs in
@@ -66,19 +67,19 @@ instance lie_module : lie_module R L (M ⊗[R] N) :=
       linear_map.ltensor_smul, lie_hom.map_smul, linear_map.add_apply], },
   lie_smul := λ c x, linear_map.map_smul _ c, }
 
-@[simp] lemma lie_tensor_right (x : L) (m : M) (n : N) :
+@[simp] lemma lie_tmul_right (x : L) (m : M) (n : N) :
   ⁅x, m ⊗ₜ[R] n⁆ = ⁅x, m⁆ ⊗ₜ n + m ⊗ₜ ⁅x, n⁆ :=
 show has_bracket_aux x (m ⊗ₜ[R] n) = _,
 by simp only [has_bracket_aux, linear_map.rtensor_tmul, to_endomorphism_apply_apply,
   linear_map.add_apply, linear_map.ltensor_tmul]
 
-variables (R L M N P)
+variables (R L M N P Q)
 
 /-- The universal property for tensor product of modules of a Lie algebra: the `R`-linear
 tensor-hom adjunction is equivariant with respect to the `L` action. -/
 def lift : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ (M ⊗[R] N →ₗ[R] P) :=
 { map_lie'  := λ x f, by
-    { ext m n, simp only [mk_apply, linear_map.compr₂_apply, lie_tensor_right, linear_map.sub_apply,
+    { ext m n, simp only [mk_apply, linear_map.compr₂_apply, lie_tmul_right, linear_map.sub_apply,
         lift.equiv_apply, linear_equiv.to_fun_eq_coe, lie_hom.lie_apply, linear_map.map_add],
       abel, },
   ..tensor_product.lift.equiv R M N P }
@@ -96,14 +97,106 @@ def lift_lie : (M →ₗ⁅R,L⁆ N →ₗ[R] P) ≃ₗ[R] (M ⊗[R] N →ₗ⁅
 ↑(maximal_trivial_equiv (lift R L M N P))).trans
 maximal_trivial_linear_map_equiv_lie_module_hom
 
-@[simp] lemma lift_lie_apply (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (m : M) (n : N) :
+@[simp] lemma coe_lift_lie_eq_lift_coe (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) :
+  ⇑(lift_lie R L M N P f) = lift R L M N P f :=
+begin
+  suffices : (lift_lie R L M N P f : M ⊗[R] N →ₗ[R] P) = lift R L M N P f,
+  { rw [← this, lie_module_hom.coe_to_linear_map], },
+  ext m n,
+  simp only [lift_lie, linear_equiv.trans_apply, lie_module_equiv.coe_to_linear_equiv,
+    coe_linear_map_maximal_trivial_linear_map_equiv_lie_module_hom, coe_maximal_trivial_equiv_apply,
+    coe_linear_map_maximal_trivial_linear_map_equiv_lie_module_hom_symm],
+end
+
+lemma lift_lie_apply (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (m : M) (n : N) :
   lift_lie R L M N P f (m ⊗ₜ n) = f m n :=
-by simp only [lift_lie, linear_equiv.trans_apply, lie_module_hom.coe_to_linear_map,
-  coe_maximal_trivial_linear_map_equiv_lie_module_hom,
-  lie_module_equiv.coe_to_linear_equiv, coe_fn_coe_base,
-  coe_maximal_trivial_linear_map_equiv_lie_module_hom_symm_apply,
-  coe_maximal_trivial_equiv_apply, lift_apply]
+by simp only [coe_lift_lie_eq_lift_coe, lie_module_hom.coe_to_linear_map, lift_apply]
+
+variables {R L M N P Q}
+
+/-- A pair of Lie module morphisms `f : M → P` and `g : N → Q`, induce a Lie module morphism:
+`M ⊗ N → P ⊗ Q`. -/
+def map (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) : M ⊗[R] N →ₗ⁅R,L⁆ P ⊗[R] Q :=
+{ map_lie' := λ x t, by
+    { simp only [linear_map.to_fun_eq_coe],
+      apply t.induction_on,
+      { simp only [linear_map.map_zero, lie_zero], },
+      { intros m n, simp only [lie_module_hom.coe_to_linear_map, lie_tmul_right,
+          lie_module_hom.map_lie, map_tmul, linear_map.map_add], },
+      { intros t₁ t₂ ht₁ ht₂, simp only [ht₁, ht₂, lie_add, linear_map.map_add], }, },
+  .. map (f : M →ₗ[R] P) (g : N →ₗ[R] Q), }
+
+@[simp] lemma coe_linear_map_map (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) :
+  (map f g : M ⊗[R] N →ₗ[R] P ⊗[R] Q) = tensor_product.map (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :=
+rfl
+
+@[simp] lemma map_tmul (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) (m : M) (n : N) :
+  map f g (m ⊗ₜ n) = (f m) ⊗ₜ (g n) :=
+map_tmul f g m n
+
+/-- Given Lie submodules `M' ⊆ M` and `N' ⊆ N`, this is the natural map: `M' ⊗ N' → M ⊗ N`. -/
+def map_incl (M' : lie_submodule R L M) (N' : lie_submodule R L N) :
+  M' ⊗[R] N' →ₗ⁅R,L⁆ M ⊗[R] N :=
+map M'.incl N'.incl
+
+@[simp] lemma map_incl_def (M' : lie_submodule R L M) (N' : lie_submodule R L N) :
+  map_incl M' N' = map M'.incl N'.incl :=
+rfl
 
 end lie_module
 
 end tensor_product
+
+namespace lie_module
+
+open_locale tensor_product
+
+variables (R) (L : Type v) (M : Type w)
+variables [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
+
+/-- The action of the Lie algebra on one of its modules, regarded as a morphism of Lie modules. -/
+def to_module_hom : L ⊗[R] M →ₗ⁅R,L⁆ M :=
+tensor_product.lie_module.lift_lie R L L M M
+{ map_lie' := λ x m, by { ext n, simp [lie_ring.of_associative_ring_bracket], },
+  ..(to_endomorphism R L M : L →ₗ[R] M →ₗ[R] M), }
+
+@[simp] lemma to_module_hom_apply (x : L) (m : M) :
+  to_module_hom R L M (x ⊗ₜ m) = ⁅x, m⁆ :=
+by simp only [to_module_hom, tensor_product.lie_module.lift_lie_apply, to_endomorphism_apply_apply,
+  lie_hom.coe_to_linear_map, lie_module_hom.coe_mk, linear_map.to_fun_eq_coe]
+
+end lie_module
+
+namespace lie_submodule
+
+open_locale tensor_product
+
+open tensor_product.lie_module
+open lie_module
+
+variables {L : Type v} {M : Type w}
+variables [lie_ring L] [lie_algebra R L]
+variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
+variables (I : lie_ideal R L) (N : lie_submodule R L M)
+
+/-- A useful alternative characterisation of Lie ideal operations on Lie submodules.
+
+Given a Lie ideal `I ⊆ L` and a Lie submodule `N ⊆ M`, by tensoring the inclusion maps and then
+applying the action of `L` on `M`, we obtain morphism of Lie modules `f : I ⊗ N → L ⊗ M → M`.
+
+This lemma states that `⁅I, N⁆ = range f`. -/
+lemma lie_ideal_oper_eq_tensor_map_range :
+  ⁅I, N⁆ = ((to_module_hom R L M).comp (map_incl I N : ↥I ⊗ ↥N →ₗ⁅R,L⁆ L ⊗ M)).range :=
+begin
+  rw [← coe_to_submodule_eq_iff, lie_ideal_oper_eq_linear_span, lie_module_hom.coe_submodule_range,
+    lie_module_hom.coe_linear_map_comp, linear_map.range_comp, map_incl_def, coe_linear_map_map,
+    tensor_product.map_range_eq_span_tmul, submodule.map_span],
+  congr, ext m, split,
+  { rintros ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, use x ⊗ₜ n, split,
+    { use [⟨x, hx⟩, ⟨n, hn⟩], simp, },
+    { simp, }, },
+  { rintros ⟨t, ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩, h⟩, rw ← h, use [⟨x, hx⟩, ⟨n, hn⟩], simp, },
+end
+
+end lie_submodule

src/field_theory/subfield.lean

@@ -286,13 +286,10 @@ variables (g : L →+* M) (f : K →+* L)
 
 /-! # range -/
 
-/-- The range of a ring homomorphism, as a subfield of the target. -/
+/-- The range of a ring homomorphism, as a subfield of the target. See Note [range copy pattern]. -/
 def field_range : subfield L :=
 ((⊤ : subfield K).map f).copy (set.range f) set.image_univ.symm
 
-/-- 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.field_range ↔ ∃ x, f x = y := iff.rfl

src/group_theory/submonoid/operations.lean

@@ -512,24 +512,47 @@ namespace monoid_hom
 
 open submonoid
 
-/-- The range of a monoid homomorphism is a submonoid. -/
+/-- For many categories (monoids, modules, rings, ...) the set-theoretic image of a morphism `f` is
+a subobject of the codomain. When this is the case, it is useful to define the range of a morphism
+in such a way that the underlying carrier set of the range subobject is definitionally
+`set.range f`. In particular this means that the types `↥(set.range f)` and `↥f.range` are
+interchangeable without proof obligations.
+
+A convenient candidate definition for range which is mathematically correct is `map ⊤ f`, just as
+`set.range` could have been defined as `f '' set.univ`. However, this lacks the desired definitional
+convenience, in that it both does not match `set.range`, and that it introduces a redudant `x ∈ ⊤`
+term which clutters proofs. In such a case one may resort to the `copy`
+pattern. A `copy` function converts the definitional problem for the carrier set of a subobject
+into a one-off propositional proof obligation which one discharges while writing the definition of
+the definitionally convenient range (the parameter `hs` in the example below).
+
+A good example is the case of a morphism of monoids. A convenient definition for
+`monoid_hom.mrange` would be `(⊤ : submonoid M).map f`. However since this lacks the required
+definitional convenience, we first define `submonoid.copy` as follows:
+```lean
+protected def copy (S : submonoid M) (s : set M) (hs : s = S) : submonoid M :=
+{ carrier  := s,
+  one_mem' := hs.symm ▸ S.one_mem',
+  mul_mem' := hs.symm ▸ S.mul_mem' }
+```
+and then finally define:
+```lean
+def mrange (f : M →* N) : submonoid N :=
+((⊤ : submonoid M).map f).copy (set.range f) set.image_univ.symm
+```
+-/
+library_note "range copy pattern"
+
+/-- The range of a monoid homomorphism is a submonoid. See Note [range copy pattern]. -/
 @[to_additive "The range of an `add_monoid_hom` is an `add_submonoid`."]
 def mrange (f : M →* N) : submonoid N :=
 ((⊤ : submonoid M).map f).copy (set.range f) set.image_univ.symm
 
-/-- 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 :=
 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 :=
 iff.rfl

src/linear_algebra/basic.lean

@@ -1378,13 +1378,10 @@ theorem comap_cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (hf p') :
   submodule.comap (cod_restrict p f hf) p' = submodule.comap f (map p.subtype p') :=
 submodule.ext $ λ x, ⟨λ h, ⟨⟨_, hf x⟩, h, rfl⟩, by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h⟩
 
-/-- The range of a linear map `f : M → M₂` is a submodule of `M₂`. -/
+/-- The range of a linear map `f : M → M₂` is a submodule of `M₂`. See Note [range copy pattern]. -/
 def range (f : M →ₗ[R] M₂) : submodule R M₂ :=
 (map f ⊤).copy (set.range f) set.image_univ.symm
 
-/-- Note that `linear_map.range` 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. -/
 theorem range_coe (f : M →ₗ[R] M₂) : (range f : set M₂) = set.range f := rfl
 
 @[simp] theorem mem_range {f : M →ₗ[R] M₂} {x} : x ∈ range f ↔ ∃ y, f y = x :=