∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 :
    ∀ (X : C) (Y : CategoryTheory.Over X),
      ((J.over X).over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)]
  [inst_2 : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat]
  [inst_3 : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat]
  {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) {I : Type u_1} (X : I → C)
  (D : (i : I) → (M.over (X i)).QuasicoherentData) (i : (i : I) × (D i).I),
  ((D i.fst).X i.snd).iteratedSliceEquiv.functor.IsContinuous ((J.over (X i.fst)).over ((D i.fst).X i.snd))
    (J.over ((D i.fst).X i.snd).left)