∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G))
  (hG : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) (a : S.Arrow) {Z : A} (h : G.obj (Opposite.op a.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift hG₀ hG s)
      (CategoryTheory.CategoryStruct.comp (G.map a.f.op) h) =
    CategoryTheory.CategoryStruct.comp (s.ι a) h