-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f g : (↑R : Type u)ᵒᵖ
i : f ⟶ g
N : ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u) := (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)
⊢ Eq (α :=
    Functor.obj
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        f ⟶
      Functor.obj
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        g)
    (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        i ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop g))
          (ModuleCat.Hom.hom
            (tilde.toOpen
              ((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op ⊤))
              (PrimeSpectrum.basicOpen (unop g))))
          (ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯))))
          ⋯))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        f)
      (ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop f))
          (ModuleCat.Hom.hom
            (tilde.toOpen
              ((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op ⊤))
              (PrimeSpectrum.basicOpen (unop f))))
          (ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯))))
          ⋯))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        i))
have hf : Eq (α :=
  LinearMap (R := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (RingHom.id (↑(CommRingCat.of (↑R : Type u)) : Type u))
    (↑(Functor.obj
          (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
            (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
          f) :
      Type u)
    (↑(Functor.obj
          (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
            (Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
          g) :
      Type u))
  (ModuleCat.Hom.hom
    (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        i ≫
      ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop g))
          (ModuleCat.Hom.hom
            (tilde.toOpen
              ((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op ⊤))
              (PrimeSpectrum.basicOpen (unop g))))
          (ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE sorry))))
          sorry)))
  (ModuleCat.Hom.hom
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        f)
      (ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (unop f))
          (ModuleCat.Hom.hom
            (tilde.toOpen
              ((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op ⊤))
              (PrimeSpectrum.basicOpen (unop f))))
          (ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE sorry))))
          sorry))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        i)))
Tactic: ext1