-- 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
c : ↥I.primeCompl
g : N →ₗ[R] M
h :
  ∀ (x : N),
    Eq (α := LocalizedModule I.primeCompl N)
      (((↑R :
                  {S : Type u_1} →
                    {M M₂ : Type (max u_1 u_2)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (S := 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) :
                      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)
                  ((LocalizedModule.map I.primeCompl :
                      (a : N →ₗ[R] M) →
                        LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I] LocalizedModule I.primeCompl M)
                    g)) ∘ₗ
              LocalizedModule.mkLinearMap I.primeCompl N :
            (a : N) → LocalizedModule I.primeCompl N)
          x :
        LocalizedModule I.primeCompl N)
      (((↑R :
                  {S : Type u_1} →
                    {M M₂ : Type (max u_1 u_2)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (S := Localization (M := R) I.primeCompl)
                ((LocalizedModule.map I.primeCompl :
                    (a : N →ₗ[R] N) →
                      LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
                  ((((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f : (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) :
                      (a : N →ₗ[R] M) → N →ₗ[R] N)
                    g)) ∘ₗ
              LocalizedModule.mkLinearMap I.primeCompl N :
            (a : N) → LocalizedModule I.primeCompl N)
          x :
        LocalizedModule I.primeCompl N)
⊢ Eq (α := N →ₗ[R] LocalizedModule I.primeCompl N)
    ((↑R :
          {S : Type u_1} →
            {M M₂ : Type (max u_1 u_2)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := 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) :
              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)
          ((LocalizedModule.map I.primeCompl :
              (a : N →ₗ[R] M) →
                LocalizedModule I.primeCompl N →ₗ[Localization.AtPrime I] LocalizedModule I.primeCompl M)
            g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N)
    ((↑R :
          {S : Type u_1} →
            {M M₂ : Type (max u_1 u_2)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := Localization (M := R) I.primeCompl)
        ((LocalizedModule.map I.primeCompl :
            (a : N →ₗ[R] N) →
              LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
          ((((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f : (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) :
              (a : N →ₗ[R] M) → N →ₗ[R] N)
            g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N)

Tactic:
ext