∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U)
  (X_1 Y_1 : TopCat.Presheaf.SheafCondition.OpensLeCover U) (f : X_1 ⟶ Y_1),
  ((TopCat.Presheaf.generateEquivalenceOpensLe_inverse' U hY).comp
          (TopCat.Presheaf.generateEquivalenceOpensLe_functor' U)).map
      f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Functor.id (TopCat.Presheaf.SheafCondition.OpensLeCover U)).map f) (CategoryTheory.eqToHom ⋯))