-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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 ⊤)
hf :
  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)
⊢ Eq (α :=
    LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u))
      (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) : 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 ⋯))))
                ⋯)) :
        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
        (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))
    (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)) ∘ₗ
      ModuleCat.Hom.hom
        (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen (unop f))))

Tactic:
dsimp [← ModuleCat.hom_comp]

Premises used: ModuleCat.hom_comp