-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  (↑a : R) • g =
    ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
          (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
        (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
      ((LinearMap.lcomp R M I.subtype : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g', a).1
⊢ Eq (α := LinearMap.{u, u, u', v'} (RingHom.id R) (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) Mₛ)
    ((↑R :
        {S M : Type u'} →
          {M₂ : Type v'} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (HSMul.hSMul (α := Rₛ) (β := ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        ((algebraMap R Rₛ : (a : R) → Rₛ) 1 : Rₛ)
        ((LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
              (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
            (((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ : (R →ₗ[R] M) →ₗ[R] Rₛ →ₗ[Rₛ] Mₛ) :
                (a : R →ₗ[R] M) → Rₛ →ₗ[Rₛ] Mₛ)
              g') :
          ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)))
    ((↑R :
        {S M : Type u'} →
          {M₂ : Type v'} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₛ)
      (((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
            (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
          (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        ((LinearMap.lcomp R M I.subtype : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g')))
have a₁ : Eq (α := ↥I →ₗ[R] Mₛ)
  ((↑R :
        {S M : Type u'} →
          {M₂ : Type v'} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (HSMul.hSMul (α := Rₛ) (β := ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        ((algebraMap R Rₛ : (a : R) → Rₛ) 1 : Rₛ)
        ((LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
              (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
            (((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ : (R →ₗ[R] M) →ₗ[R] Rₛ →ₗ[Rₛ] Mₛ) :
                (a : R →ₗ[R] M) → Rₛ →ₗ[Rₛ] Mₛ)
              g') :
          ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)) ∘ₗ
    Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I)
  ((↑R :
        {S M : Type u'} →
          {M₂ : Type v'} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₛ)
      (((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
            (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
          (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        ((LinearMap.lcomp R M I.subtype : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g')) ∘ₗ
    Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I)
Tactic: refine IsLocalizedModule.linearMap_ext S (I.toLocalized' Rₛ S (Algebra.linearMap R Rₛ)) f ?_