-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
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_1 : 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_1 ∘ₗ
          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_1)))
    id
f :
  LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
    (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)
h :
  Membership.mem (γ :=
      Submodule R
        (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
          (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
      (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
        ((fun (P : Ideal R) (x : P.IsMaximal) ↦
            (LocalizedModule.map P.primeCompl :
              (N →ₗ[R] N) →ₗ[R]
                LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                  (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
          I hI)
        (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
          ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f_1)))
      f →
    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_1)))
      f
⊢ Membership.mem (γ :=
      Submodule R
        (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
          (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
      (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
        ((fun (P : Ideal R) (x : P.IsMaximal) ↦
            (LocalizedModule.map P.primeCompl :
              (N →ₗ[R] N) →ₗ[R]
                LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                  (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
          I hI)
        (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
          ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f_1)))
      f ↔
    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_1)))
      f
have h₁ : 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_1)))
    f →
  Membership.mem (γ :=
    Submodule R
      (LinearMap (R := Localization (M := R) I.primeCompl) (RingHom.id (Localization (M := R) I.primeCompl))
        (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl N)))
    (Submodule.localized₀ (M := N →ₗ[R] N) I.primeCompl
      ((fun (P : Ideal R) (x : P.IsMaximal) ↦
          (LocalizedModule.map P.primeCompl :
            (N →ₗ[R] N) →ₗ[R]
              LinearMap (R := Localization (M := R) P.primeCompl) (RingHom.id (Localization (M := R) P.primeCompl))
                (LocalizedModule P.primeCompl N) (LocalizedModule P.primeCompl N)))
        I hI)
      (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
        ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f_1)))
    f
Tactic: constructor