Theorem: ExtrDisc.Sheaf.isSheafColimit (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
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
Tactic:
apply isSheafColimitAux
State after:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)

State before:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ ∀ (j : J), Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)
Tactic:
intro j
State after:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
j : J
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)

State before:
case h
A : Type (u + 2)
inst✝⁴ : Category A
inst✝³ : HasZeroMorphisms A
inst✝² : HasFiniteBiproducts A
J : Type (u + 1)
inst✝¹ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
inst✝ : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
j : J
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) ((F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A).obj j)
Tactic:
apply Sheaf.cond
State after:
no goals