∀ {C₀ : Type u_6} {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_6} C₀]
  [inst_1 : CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.Functor C₀ C}
  {J₀ : CategoryTheory.GrothendieckTopology C₀} {J : CategoryTheory.GrothendieckTopology C} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{u_3, u_4} 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)) (x : s.pt ⟶ (S.multifork G).pt),
  (∀ (i : S.shape.L), CategoryTheory.CategoryStruct.comp x ((S.multifork G).ι i) = s.ι i) →
    x = CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift hG₀ hG s