-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u_1, u_1, uM, u_5} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective.{u_4, u_5} (Rₚ I) (Mₚ I)
inst_11 : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : RingEquiv.{u_4, u_1} (Rₚ P) (Localization.AtPrime P) :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P))
m : Mₚ P
r : R
s : ↥P.primeCompl
H₁ :
  Eq (α := LocalizedModule P.primeCompl M)
    ((((algebraMap R (End R (LocalizedModule P.primeCompl M)) : (a : R) → End R (LocalizedModule P.primeCompl M))
              (↑s : R) :
            End R (LocalizedModule P.primeCompl M)) :
          (a : LocalizedModule P.primeCompl M) → LocalizedModule P.primeCompl M)
        (AddHom.toFun
          (LinearMap.toAddHom
            (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
              Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
          (HSMul.hSMul.{u_4, u_5, u_5} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m)) :
      LocalizedModule P.primeCompl M)
    ((((algebraMap R (End R (LocalizedModule P.primeCompl M)) : (a : R) → End R (LocalizedModule P.primeCompl M))
              (↑s : R) :
            End R (LocalizedModule P.primeCompl M)) :
          (a : LocalizedModule P.primeCompl M) → LocalizedModule P.primeCompl M)
        (HSMul.hSMul (α := Localization.AtPrime P)
          ((((↑e : RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
                RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
              (a : Rₚ P) → Localization.AtPrime P)
            (IsLocalization.mk' (Rₚ P) r s))
          (AddHom.toFun
            (LinearMap.toAddHom
              (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
                Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
            m)) :
      LocalizedModule P.primeCompl M)
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
          Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
      (HSMul.hSMul.{u_4, u_5, u_5} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m) =
    HSMul.hSMul (α := Localization.AtPrime P)
      ((((↑e : RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
            RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
          (a : Rₚ P) → Localization.AtPrime P)
        (IsLocalization.mk' (Rₚ P) r s))
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        m)

Tactic:
apply ((Module.End.isUnit_iff _).mp
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap P.primeCompl M) s)).1

Premises used: Module.End.isUnit_iff, And.left, Iff.mp, LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units