-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
N : Type u_2
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
inst_5 : Module.FinitePresentation R N
H :
  ∀ (I : Ideal R) (x : I.IsMaximal),
    ∃ (g :
      LinearMap (R := Localization.AtPrime I) (RingHom.id (Localization.AtPrime I)) (LocalizedModule I.primeCompl N)
        (LocalizedModule I.primeCompl M)),
      (LocalizedModule.map I.primeCompl :
              (a : M →ₗ[R] N) →
                LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
            f ∘ₗ
          g =
        id
I : Ideal R
hI : I.IsMaximal
this :
  Membership.mem (γ :=
    Submodule (Localization (M := R) I.primeCompl)
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (range (R := Localization (M := R) I.primeCompl) (M :=
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization.AtPrime I))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M))
      (τ₁₂ := RingHom.id (Localization (M := R) I.primeCompl))
      ((llcomp (Localization (M := R) I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N) :
          (a : LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
            (LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I]
                LocalizedModule I.primeCompl M) →ₗ[Localization I.primeCompl]
              LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        ((LocalizedModule.map I.primeCompl :
            (a : M →ₗ[R] N) →
              LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
          f)))
    id
g : N →ₗ[R] M
s : ↥I.primeCompl
h :
  Eq (α :=
    LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
      (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
    ((((algebraMap R
                  (Module.End R
                    (LinearMap (R := Localization (M := R) I.primeCompl)
                      (RingHom.id (Localization (M := R) I.primeCompl)) (LocalizedModule I.primeCompl N)
                      (LocalizedModule I.primeCompl N))) :
                (a : R) →
                  Module.End R
                    (LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N))
              (↑s : R) :
            Module.End R
              (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
                (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))) :
          (a : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
            LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (f ∘ₗ g) s) :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
    ((((algebraMap R
                  (Module.End R
                    (LinearMap (R := Localization (M := R) I.primeCompl)
                      (RingHom.id (Localization (M := R) I.primeCompl)) (LocalizedModule I.primeCompl N)
                      (LocalizedModule I.primeCompl N))) :
                (a : R) →
                  Module.End R
                    (LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N))
              (↑s : R) :
            Module.End R
              (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
                (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))) :
          (a : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
            LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
        ((((llcomp (Localization (M := R) I.primeCompl) (LocalizedModule I.primeCompl N)
                    (LocalizedModule I.primeCompl M) (LocalizedModule I.primeCompl N) :
                  (a : LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
                    (LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I]
                        LocalizedModule I.primeCompl M) →ₗ[Localization I.primeCompl]
                      LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
                ((LocalizedModule.map I.primeCompl :
                    (a : M →ₗ[R] N) →
                      LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
                  f) :
              LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
                (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization.AtPrime I))
                  (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M))
                (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
                  (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))) :
            (a : LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I] LocalizedModule I.primeCompl M) →
              LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
          (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s)) :
      LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))
⊢ IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) (f ∘ₗ g) s =
    (((llcomp (Localization (M := R) I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
                (LocalizedModule I.primeCompl N) :
              (a : LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N) →
                (LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I]
                    LocalizedModule I.primeCompl M) →ₗ[Localization I.primeCompl]
                  LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
            ((LocalizedModule.map I.primeCompl :
                (a : M →ₗ[R] N) →
                  LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
              f) :
          LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
            (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization.AtPrime I))
              (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M))
            (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
              (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N))) :
        (a : LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I] LocalizedModule I.primeCompl M) →
          LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
      (IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g s)

Tactic:
apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units
         (LocalizedModule.map I.primeCompl) s).injective

Premises used: LocalizedModule.map, Module.End.isUnit_iff, Function.Bijective.injective, Iff.mp, Ideal.primeCompl, IsLocalizedModule.map_units