∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C)
  {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  TopCat.Presheaf.IsSheaf (⋯.functor.op.comp X.presheaf)