-- 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 (α := 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)
have a : ∀ (x : M),
  Eq.{u_3 + 1} (α := 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 :
          (a : M) → M')
        x :
      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₂)
              (S := Rₛ) LinearMap.id ∘ₗ
            f :
          (a : M) → M')
        x :
      M')
Tactic: ext