∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D},
  CategoryTheory.CompatiblePreserving K G →
    ∀ (ℱ : CategoryTheory.Sheaf K (Type w)) {Z : C} {T : CategoryTheory.Presieve Z}
      {x : CategoryTheory.Presieve.FamilyOfElements (G.op.comp ℱ.val) T},
      x.Compatible →
        ∀ {Y : C} {f : Y ⟶ Z} (hf : T f),
          CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x (G.map f) ⋯ = x f hf