∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
  J₁.close (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f (J₁.close S)