-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
⊢ 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)))))))
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext r : 3