-- Module: Mathlib.RingTheory.LocalProperties.Injective
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
a₁ :
  ∀ (x : ↥I),
    Eq.{v' + 1} (α := 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 :
            (a : ↥I) → Mₛ)
          x :
        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')) ∘ₗ
              Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I :
            (a : ↥I) → Mₛ)
          x :
        Mₛ)
⊢ 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:
ext