-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑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))))
have 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)) sorry) :
        (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)) sorry) :
        (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)))))))
Tactic: apply (TopCat.Sheaf.restrictHomEquivHom _ _ PrimeSpectrum.isBasis_basic_opens).symm.injective