-- 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 ⊤)
⊢ ModuleCat.Hom.hom
      (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f)) ≫
        (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
            i.unop.hom.op ≫
          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
      (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop 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 ⋯))))
              ⋯) ≫
          (Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
            i.unop.hom.op)
have hf : ModuleCat.Hom.hom
    (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop g)) ≫
      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
    (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop 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) ≫
        (Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
          i.unop.hom.op)
Tactic: rw [tilde.toOpen_res_assoc]