Theorem: ExtrDisc.Sheaf.isSheafColimitAux (Condensed/ExtrDiscSheafCondition.lean)

State before:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F : J ⥤ ExtrDiscᵒᵖ ⥤ A
inst✝ : HasColimit F
h : ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) (F.obj j)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit F)
Tactic:
rw [sheafCondition]
State after:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F : J ⥤ ExtrDiscᵒᵖ ⥤ A
inst✝ : HasColimit F
h : ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) (F.obj j)
⊢ Nonempty (PreservesFiniteProducts (colimit F))

State before:
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F : J ⥤ ExtrDiscᵒᵖ ⥤ A
inst✝ : HasColimit F
h : ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) (F.obj j)
⊢ Nonempty (PreservesFiniteProducts (colimit F))
Tactic:
exact ⟨preservesFiniteProducts _ h⟩
State after:
no goals