-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
M' : Type u_1
inst_5 : AddCommGroup M'
inst_6 : Module R M'
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
N' : Type u_2
inst_8 : AddCommGroup N'
inst_9 : Module R N'
g : N →ₗ[R] N'
inst_10 : IsLocalizedModule S g
inst_11 : FinitePresentation R M
inst_12 : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • (↑l : M' →ₗ[R] N') ∘ₗ f
this_1 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l' : M' →ₗ[R] N') : (a : M') → N')
r : R
hr : r ∈ S
hr' :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) N)
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] N) →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) N)
                l' :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) N)) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) N)
rs : Submonoid R := Submonoid.powers (r * (↑s : R))
Rᵣₛ : Type u_3 := Localization (M := R) rs
hsu : IsUnit (M := Rᵣₛ) ((algebraMap R Rᵣₛ : (a : R) → Rᵣₛ) (↑s : R) : Rᵣₛ)
this :
  Function.Bijective (α := LocalizedModule rs M) (β := LocalizedModule rs N)
    (⇑(HSMul.hSMul (β :=
          LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs)) (LocalizedModule rs M)
            (LocalizedModule rs N))
          (↑hsu.unit⁻¹ : Rᵣₛ)
          ((LocalizedModule.map rs : (a : M →ₗ[R] N) → LocalizedModule rs M →ₗ[Localization rs] LocalizedModule rs N)
              l' :
            LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs)) (LocalizedModule rs M)
              (LocalizedModule rs N))) :
      (a : LocalizedModule rs M) → LocalizedModule rs N)
x : M
⊢ Eq.{u_2 + 1} (α := N')
    ((((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
        (((LocalizedModule.lift (Submonoid.powers (r * (↑s : R))) g ⋯ ∘ₗ
                  (↑R :
                      {S : Type u_3} →
                        {M : Type (max u_3 u_4)} →
                          {M₂ : Type (max u_3 u_5)} →
                            [inst : Semiring R] →
                              [inst_13 : Semiring S] →
                                [inst_14 : AddCommMonoid M] →
                                  [inst_15 : AddCommMonoid M₂] →
                                    [inst_16 : Module R M] →
                                      [inst_17 : Module R M₂] →
                                        [inst_18 : Module S M] →
                                          [inst_19 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (↑(LinearEquiv.ofBijective
                          (HSMul.hSMul (β :=
                            LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs))
                              (LocalizedModule rs M) (LocalizedModule rs N))
                            (↑hsu.unit⁻¹ : Rᵣₛ)
                            ((LocalizedModule.map rs :
                                  (a : M →ₗ[R] N) → LocalizedModule rs M →ₗ[Localization rs] LocalizedModule rs N)
                                l' :
                              LinearMap (R := Localization (M := R) rs) (RingHom.id (Localization (M := R) rs))
                                (LocalizedModule rs M) (LocalizedModule rs N)))
                          this) :
                      LocalizedModule.Away (r * (↑s : R)) M →ₗ[Localization (Submonoid.powers (r * (↑s : R)))]
                        LocalizedModule.Away (r * (↑s : R)) N)) ∘ₗ
                LocalizedModule.mkLinearMap rs M :
              (a : M) → N')
            x :
          N') :
      N')
    ((((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
        ((((↑l : M' →ₗ[R] N') ∘ₗ LocalizedModule.lift (Submonoid.powers (r * (↑s : R))) f ⋯) ∘ₗ
                LocalizedModule.mkLinearMap rs M :
              (a : M) → N')
            x :
          N') :
      N')
have this₁ : ∀ (x : M),
  (g : (a : N) → N') ((l' : (a : M) → N) x : N) =
    HSMul.hSMul (β := N') (↑s : R) ((l : (a : M') → N') ((f : (a : M) → M') x : M') : N')
Tactic: have : ∀ x, g (l' x) = s.1 • (l (f x)) := LinearMap.congr_fun H