∀ {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X)
  (X_1 : TopologicalSpace.OpenNhds x),
  h.functor.map (CategoryTheory.CategoryStruct.id X_1) = CategoryTheory.CategoryStruct.id ⟨h.functor.obj ↑X_1, ⋯⟩