-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
h :
  Eq (α :=
    Quiver.Hom (V :=
      (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
            basicOpen)ᵒᵖ ⥤
        ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u))
      (Functor.op (inducedFunctor basicOpen) ⋙
        (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
      (Functor.op (inducedFunctor basicOpen) ⋙
        (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u)))))))
    ((Equiv.symm
            (Sheaf.restrictHomEquivHom
              ((Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)) ⋯) :
          (a :
              (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj ⟶
                (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj) →
            (inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj ⟶
              (inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj)
        (InducedCategory.Hom.hom
          (CategoryTheory.Functor.map modulesSpecToSheaf
            ((tilde.functor R).map (NatTrans.app (Iso.hom toTildeΓNatIso) M) ≫
              NatTrans.app fromTildeΓNatTrans ((tilde.functor R).obj M)))) :
      Quiver.Hom (V :=
        (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u))
              (Opens ↥(Spec (CommRingCat.of (↑R : Type u)))) basicOpen)ᵒᵖ ⥤
          ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u))
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u)))))))
    ((Equiv.symm
            (Sheaf.restrictHomEquivHom
              ((Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)) ⋯) :
          (a :
              (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj ⟶
                (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj) →
            (inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj ⟶
              (inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj)
        (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 ((tilde.functor R).obj M)))) :
      Quiver.Hom (V :=
        (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u))
              (Opens ↥(Spec (CommRingCat.of (↑R : Type u)))) basicOpen)ᵒᵖ ⥤
          ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u))
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u)))))))
⊢ Eq (α :=
    (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))) ⟶
      (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map modulesSpecToSheaf
        ((tilde.functor R).map (NatTrans.app (Iso.hom toTildeΓNatIso) M) ≫
          NatTrans.app fromTildeΓNatTrans ((tilde.functor R).obj M))))
    (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 ((tilde.functor R).obj M))))

Tactic:
apply (TopCat.Sheaf.restrictHomEquivHom _ _ PrimeSpectrum.isBasis_basic_opens).symm.injective

Premises used: TopCat.Sheaf.restrictHomEquivHom, Equiv.injective, Equiv.symm