∀ {X Y : TopCat} (H : X ≅ Y) (X_1 : TopologicalSpace.Opens ↑Y),
  CategoryTheory.CategoryStruct.comp
      ((TopologicalSpace.Opens.map H.hom).map
        ((CategoryTheory.NatIso.ofComponents (fun U => CategoryTheory.eqToIso ⋯) ⋯).hom.app X_1))
      ((CategoryTheory.NatIso.ofComponents (fun U => CategoryTheory.eqToIso ⋯) ⋯).hom.app
        ((TopologicalSpace.Opens.map H.hom).obj X_1)) =
    CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.map H.hom).obj X_1)