Theorem: ExtrDisc.Sheaf.isSheafOfIsColimit (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
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Tactic:
have : HasColimit (F ⋙ sheafToPresheaf _ _) := ⟨S,hS⟩
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
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt

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
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Tactic:
let e : S.pt ≅ colimit (F ⋙ sheafToPresheaf _ _) := 
  hS.coconePointUniqueUpToIso (colimit.isColimit _)
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
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt

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
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Tactic:
rw [Presheaf.isSheaf_of_iso_iff e]
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
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))

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
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
Tactic:
apply isSheafColimit
State after:
no goals