-- Lean 4 proof step from Mathlib.RingTheory.Localization.Module (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
N : Type u_4
N' : Type u_5
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid N'
inst_8 : Module R N
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
Rₛ : Type u_6
inst_11 : CommSemiring Rₛ
inst_12 : Algebra R Rₛ
inst_13 : Module Rₛ M'
inst_14 : Module Rₛ N'
inst_15 : IsScalarTower R Rₛ M'
inst_16 : IsScalarTower R Rₛ N'
inst_17 : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ Eq.{u_3 + 1} (α := M' →ₗ[R] M')
    ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
          (↑e.symm : N →ₗ[R] M) ∘ₗ
        ((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N')
          (↑e : M →ₗ[R] N)))
    ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₛ) LinearMap.id)
have a : Eq (α := M →ₗ[R] M')
  ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (((mapExtendScalars S g f Rₛ : (N →ₗ[R] M) →ₗ[R] N' →ₗ[Rₛ] M') : (a : N →ₗ[R] M) → N' →ₗ[Rₛ] M')
          (↑e.symm : N →ₗ[R] M) ∘ₗ
        ((mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N') : (a : M →ₗ[R] N) → M' →ₗ[Rₛ] N')
          (↑e : M →ₗ[R] N)) ∘ₗ
    f)
  ((↑R :
        {S : Type u_6} →
          {M M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_18 : Semiring S] →
                [inst_19 : AddCommMonoid M] →
                  [inst_20 : AddCommMonoid M₂] →
                    [inst_21 : Module R M] →
                      [inst_22 : Module R M₂] →
                        [inst_23 : Module S M] →
                          [inst_24 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₛ) LinearMap.id ∘ₗ
    f)
Tactic: apply IsLocalizedModule.linearMap_ext S f f