∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] (X Y : C)
  (u : Y ⟶ X),
  ∀ s ∈ (CategoryTheory.Precoverage.finite C).coverings X,
    CategoryTheory.Presieve.pullbackArrows u s ∈ (CategoryTheory.Precoverage.finite C).coverings Y