-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
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 : Module.Finite R M
inst_12 : Module.FinitePresentation R N
l : M →ₗ[R] N
hf :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := M') (β := N')
    (⇑((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l : M' →ₗ[R] N') : (a : M') → N')
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • (↑e.symm : N' →ₗ[R] M') ∘ₗ g
H₁ : g ∘ₗ l ∘ₗ l' = g ∘ₗ HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
s₁ : ↥S
hs₁ : s₁ • l ∘ₗ l' = s₁ • HSMul.hSMul (β := N →ₗ[R] N) s₀ LinearMap.id
H₂ : f ∘ₗ l' ∘ₗ l = f ∘ₗ HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
s₂ : ↥S
hs₂ : s₂ • l' ∘ₗ l = s₂ • HSMul.hSMul (β := M →ₗ[R] M) s₀ LinearMap.id
t : R
ht : (↑s₀ : R) * (↑s₁ : R) * (↑s₂ : R) ∣ t
Rₛ : Type u_3 := Localization (Submonoid.powers t)
lₛ : LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
  (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
hu :
  IsUnit (M := Rₛ)
    ((algebraMap R Rₛ : (a : R) → Rₛ)
        (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers t) x) t ⋯) : R) :
      Rₛ)
hu₀ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₀ : R) : Rₛ)
hu₁ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₁ : R) : Rₛ)
hu₂ : IsUnit (M := Rₛ) ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₂ : R) : Rₛ)
lₛ' : LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
  (LocalizedModule (Submonoid.powers t) N) (LocalizedModule (Submonoid.powers t) M) :=
  (LocalizedModule.map (Submonoid.powers t) :
      (a : N →ₗ[R] M) →
        LocalizedModule (Submonoid.powers t) N →ₗ[Localization (Submonoid.powers t)]
          LocalizedModule (Submonoid.powers t) M)
    l'
⊢ Eq (α :=
    LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
      (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))
    ((((algebraMap Rₛ
                  (Module.End Rₛ
                    (LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                      (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))) :
                (a : Rₛ) →
                  Module.End Rₛ
                    (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M))
              ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₀ : R)) :
            Module.End Rₛ
              (LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))) :
          (a :
              LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                LocalizedModule (Submonoid.powers t) M) →
            LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
              LocalizedModule (Submonoid.powers t) M)
        ((((algebraMap Rₛ
                    (Module.End Rₛ
                      (LinearMap (R := Localization (Submonoid.powers t))
                        (RingHom.id (Localization (Submonoid.powers t))) (LocalizedModule (Submonoid.powers t) M)
                        (LocalizedModule (Submonoid.powers t) M))) :
                  (a : Rₛ) →
                    Module.End Rₛ
                      (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                        LocalizedModule (Submonoid.powers t) M))
                ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₂ : R)) :
              Module.End Rₛ
                (LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                  (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))) :
            (a :
                LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                  LocalizedModule (Submonoid.powers t) M) →
              LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                LocalizedModule (Submonoid.powers t) M)
          (((↑hu₀.unit⁻¹ : Rₛ) • lₛ') ∘ₗ lₛ)) :
      LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
        (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))
    ((((algebraMap Rₛ
                  (Module.End Rₛ
                    (LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                      (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))) :
                (a : Rₛ) →
                  Module.End Rₛ
                    (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M))
              ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₀ : R)) :
            Module.End Rₛ
              (LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))) :
          (a :
              LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                LocalizedModule (Submonoid.powers t) M) →
            LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
              LocalizedModule (Submonoid.powers t) M)
        ((((algebraMap Rₛ
                    (Module.End Rₛ
                      (LinearMap (R := Localization (Submonoid.powers t))
                        (RingHom.id (Localization (Submonoid.powers t))) (LocalizedModule (Submonoid.powers t) M)
                        (LocalizedModule (Submonoid.powers t) M))) :
                  (a : Rₛ) →
                    Module.End Rₛ
                      (LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                        LocalizedModule (Submonoid.powers t) M))
                ((algebraMap R Rₛ : (a : R) → Rₛ) (↑s₂ : R)) :
              Module.End Rₛ
                (LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                  (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))) :
            (a :
                LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                  LocalizedModule (Submonoid.powers t) M) →
              LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                LocalizedModule (Submonoid.powers t) M)
          LinearMap.id) :
      LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
        (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))
have a : (↑s₂ : R) • (↑s₀ : R) • ((↑hu₀.unit⁻¹ : Rₛ) • lₛ') ∘ₗ lₛ =
  (↑s₂ : R) •
    HSMul.hSMul (β :=
      LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
        (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M))
      (↑s₀ : R) LinearMap.id
Tactic: simp only [Module.algebraMap_end_apply, algebraMap_smul, LinearMap.map_smul_of_tower]