∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C} (X : C)
  (S : CategoryTheory.Sieve X), J.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), J.Saturate Y (CategoryTheory.Sieve.pullback f S)