-- 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 (α := ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
    ((((algebraMap Rₛ (End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)) :
                (a : Rₛ) → End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ))
              ((algebraMap R Rₛ : (a : R) → Rₛ) (↑a : R)) :
            End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)) :
          (a : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) →
            ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        ((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ₛ)
          (HSMul.hSMul (β := Rₛ →ₗ[Rₛ] Mₛ) (IsLocalization.mk' Rₛ 1 a)
            (((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ : (R →ₗ[R] M) →ₗ[R] Rₛ →ₗ[Rₛ] Mₛ) :
                  (a : R →ₗ[R] M) → Rₛ →ₗ[Rₛ] Mₛ)
                g' :
              Rₛ →ₗ[Rₛ] Mₛ))) :
      ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
    ((((algebraMap Rₛ (End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)) :
                (a : Rₛ) → End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ))
              ((algebraMap R Rₛ : (a : R) → Rₛ) (↑a : R)) :
            End Rₛ (↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)) :
          (a : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) →
            ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        g :
      ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
have a₁ : 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ₛ) =
  ((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')
Tactic: simp_rw [algebraMap_end_apply, map_smul, ← mul_smul, algebraMap_smul, IsLocalization.mk'_spec', e]