-- 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 ⊤)
x : (↑((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)) : Type u)
hf :
  Eq (α :=
    (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
          (op (PrimeSpectrum.basicOpen (unop g)))) :
      Type u))
    ((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 ⋯))) :
          (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop g)))) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop g)))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
            LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X :=
            (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op ⊤))
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              (Quiver.Hom.op (homOfLE ⋯) ≫ i.unop.hom.op)) :
          (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop g)))) : Type u))
        x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop g)))) :
        Type u))
⊢ Eq (α :=
    (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
          (op (PrimeSpectrum.basicOpen (unop g)))) :
      Type u))
    ((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 ⋯))))
            ⋯ :
          (a :
              (↑((modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).presheaf.obj
                    (op (PrimeSpectrum.basicOpen (unop g)))) :
                Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop g)))) : Type u))
        ((ModuleCat.Hom.hom
                (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤))
                  (PrimeSpectrum.basicOpen (unop g))) :
              (a : (↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) : Type u)) →
                (↑((modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).presheaf.obj
                      (op (PrimeSpectrum.basicOpen (unop g)))) :
                  Type u))
            x :
          (↑((Functor.obj modulesSpecToSheaf
                      (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).presheaf.obj
                (op (PrimeSpectrum.basicOpen (unop g)))) :
            Type u)) :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop g)))) :
        Type u))
    ((ModuleCat.Hom.hom
            ((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
              i.unop.hom.op) :
          (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f)))) : Type u)) →
            (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop g)))) : Type u))
        ((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 ⋯))))
                ⋯ :
              (a :
                  (↑((modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj.obj
                        (op (PrimeSpectrum.basicOpen (unop f)))) :
                    Type u)) →
                (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f)))) : Type u))
            ((ModuleCat.Hom.hom
                    (tilde.toOpen ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤))
                      (PrimeSpectrum.basicOpen (unop f))) :
                  (a : (↑((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) : Type u)) →
                    (↑((modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).obj.obj
                          (op (PrimeSpectrum.basicOpen (unop f)))) :
                      Type u))
                x :
              (↑((Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj
                        (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                    (op (PrimeSpectrum.basicOpen (unop f)))) :
                Type u)) :
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (PrimeSpectrum.basicOpen (unop f)))) :
            Type u)) :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop g)))) :
        Type u))

Tactic:
simp only [IsLocalizedModule.lift_apply, ← ModuleCat.comp_apply, ← Functor.map_comp]

Premises used: ModuleCat.comp_apply, IsLocalizedModule.lift_apply, CategoryTheory.Functor.map_comp