[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{max v u, w} D
inst✝ : Abelian D
J : GrothendieckTopology C
j : ℕ
F : Discrete (Fin j) ⥤ Sheaf J D
⊢ HasLimit F
[PROOFSTEP]
infer_instance
