-- 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 (α :=
    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 ⋯))))
            ⋯)))
    (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 ⋯))))
            ⋯))
        (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 : ∀ (x : ↥(Submonoid.powers (unop f))),
  IsUnit (M :=
    Module.End (↑R : 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))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : 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)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g) : Type u))
        (↑x : (↑R : Type u)) :
      Module.End (↑R : 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))
Tactic: apply IsLocalizedModule.ext (.powers (M := R) f.unop)
          (tilde.toOpen _ (PrimeSpectrum.basicOpen (R := R) f.unop)).hom