awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
rw : PreservesFiniteProducts (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt
⊢ Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Tactic:
rw [Presheaf.isSheaf_iff_preservesFiniteProducts]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} C
inst_3 : Category.{v_3, u_3} J
inst_4 : FinitaryExtensive.{v_2, u_2} C
inst_5 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_6 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
inst : PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)

Tactic:
apply +allowSynthFailures comp_preservesFiniteProducts

Premises used: CategoryTheory.Limits.comp_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
i : J
rw : Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
i : J
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
(G.obj i).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
i : J
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
exact (G.obj i).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
⊢ ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
have : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf _ A).obj i) := fun i ↦ by
    rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]
    exact (G.obj i).property
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
this : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip

Tactic:
⟨fun _ ↦ preservesLimitsOfShape_of_evaluation _ _ fun d ↦
    inferInstanceAs (PreservesLimitsOfShape _ ((G ⋙ sheafToPresheaf _ _).obj d))⟩

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation, _private.0.CategoryTheory.isSheaf_pointwiseColimit._proof_1, CategoryTheory.Limits.PreservesFiniteProducts.mk, Fin, CategoryTheory.extensiveTopology, CategoryTheory.Discrete, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
this : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip

Tactic:
exact ⟨fun _ ↦ preservesLimitsOfShape_of_evaluation _ _ fun d ↦
    inferInstanceAs (PreservesLimitsOfShape _ ((G ⋙ sheafToPresheaf _ _).obj d))⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst_1 : Category.{v_1, u_1} A
inst_2 : Category.{v_2, u_2} C
inst_3 : Category.{v_3, u_3} J
inst_4 : FinitaryExtensive.{v_2, u_2} C
inst_5 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_6 : Preadditive.{v_1, u_1} A
x : ℕ
inst : PreservesBiproductsOfShape (C := Functor.{v_3, v_1, u_3, u_1} J A) (Fin x) colim
⊢ PreservesLimitsOfShape (C := Functor.{v_3, v_1, u_3, u_1} J A) (Discrete (Fin x)) colim

Tactic:
apply +allowSynthFailures preservesProductsOfShape_of_preservesBiproductsOfShape

Premises used: CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : Preadditive.{v_1, u_1} A
x : ℕ
⊢ PreservesBiproductsOfShape (C := Functor.{v_3, v_1, u_3, u_1} J A) (Fin x) colim

Tactic:
apply preservesBiproductsOfShape_of_preservesCoproductsOfShape

Premises used: CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
suffices : CreatesColimit G (sheafToPresheaf (extensiveTopology C) A)
⊢ PreservesColimit G (sheafToPresheaf (extensiveTopology C) A)

Tactic:
suffices CreatesColimit G (sheafToPresheaf (extensiveTopology C) A) from inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
refine :
  ∀ (c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)) (hc : IsColimit c),
    Presheaf.IsSheaf (extensiveTopology C) c.pt
⊢ CreatesColimit G (sheafToPresheaf (extensiveTopology C) A)

Tactic:
refine createsColimitOfIsSheaf _ (fun c hc ↦ ?_)

Premises used: CategoryTheory.Sheaf.createsColimitOfIsSheaf
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
i : c.pt ≅ (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim :=
  hc.coconePointUniqueUpToIso (pointwiseIsColimit (G ⋙ sheafToPresheaf (extensiveTopology C) A))
rw : Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)
⊢ Presheaf.IsSheaf (extensiveTopology C) c.pt

Tactic:
rw [Presheaf.isSheaf_of_iso_iff i]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
i : c.pt ≅ (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim :=
  hc.coconePointUniqueUpToIso (pointwiseIsColimit (G ⋙ sheafToPresheaf (extensiveTopology C) A))
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)

Tactic:
isSheaf_pointwiseColimit _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.isSheaf_pointwiseColimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
Goal:
A : Type u_1
C : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} C
inst_2 : Category.{v_3, u_3} J
inst_3 : FinitaryExtensive.{v_2, u_2} C
inst_4 : HasColimitsOfShape.{v_3, u_3, v_1, u_1} J A
inst_5 : PreservesFiniteProducts (C := Functor.{v_3, v_1, u_3, u_1} J A) colim
G : J ⥤ Sheaf.{v_2, v_1, u_2, u_1} (extensiveTopology C) A
c : Cocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)
hc : IsColimit c
i : c.pt ≅ (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim :=
  hc.coconePointUniqueUpToIso (pointwiseIsColimit (G ⋙ sheafToPresheaf (extensiveTopology C) A))
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)

Tactic:
exact isSheaf_pointwiseColimit _

Premises used: CategoryTheory.isSheaf_pointwiseColimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Presieve.{v_1, u_1} X
inst_3 : S.Extensive
obtain :
  ∀ (w : Type),
    Finite w →
      ∀ (w_2 : w → C) (w_3 : (a : w) → w_2 a ⟶ X) [(ofArrows w_2 w_3).Extensive] (hc : IsColimit (Cofan.mk X w_3))
        {Y Z : C} {f : Y ⟶ X}, ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, S f → ∀ {g : Z ⟶ X}, S g → HasPullback f g

Tactic:
obtain ⟨_, _, _, _, rfl, ⟨hc⟩⟩ := Presieve.Extensive.arrows_nonempty_isColimit (R := S)

Premises used: CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
w : Type
w_1 : Finite w
w_2 : w → C
w_3 : (a : w) → w_2 a ⟶ X
inst_3 : (ofArrows w_2 w_3).Extensive
hc : IsColimit (Cofan.mk X w_3)
Y : C
_ : ∀ {Z : C} {f : Y ⟶ X}, ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g
⊢ ∀ {Z : C} {f : Y ⟶ X}, ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
w : Type
w_1 : Finite w
w_2 : w → C
w_3 : (a : w) → w_2 a ⟶ X
inst_3 : (ofArrows w_2 w_3).Extensive
hc : IsColimit (Cofan.mk X w_3)
Y Z : C
_ : ∀ {f : Y ⟶ X}, ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g
⊢ ∀ {f : Y ⟶ X}, ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
w : Type
w_1 : Finite w
w_2 : w → C
w_3 : (a : w) → w_2 a ⟶ X
inst_3 : (ofArrows w_2 w_3).Extensive
hc : IsColimit (Cofan.mk X w_3)
Y Z : C
f : Y ⟶ X
_ : ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g
⊢ ofArrows w_2 w_3 f → ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
w : Type
w_1 : Finite w
w_2 : w → C
w_3 : (a : w) → w_2 a ⟶ X
inst_3 : (ofArrows w_2 w_3).Extensive
hc : IsColimit (Cofan.mk X w_3)
Y Z : C
f : Y ⟶ X
h : ofArrows w_2 w_3 f
_ : ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g
⊢ ∀ {g : Z ⟶ X}, ofArrows w_2 w_3 g → HasPullback f g

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
w : Type
w_1 : Finite w
w_2 : w → C
w_3 : (a : w) → w_2 a ⟶ X
inst_3 : (ofArrows w_2 w_3).Extensive
hc : IsColimit (Cofan.mk X w_3)
Y Z : C
f : Y ⟶ X
h : ofArrows w_2 w_3 f
g : Z ⟶ X
hg : ofArrows w_2 w_3 g
mk : ∀ (i : w), HasPullback f (w_3 i)
⊢ HasPullback f g

Tactic:
cases hg
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
X : C
w : Type
w_1 : Finite w
w_2 : w → C
w_3 : (a : w) → w_2 a ⟶ X
inst_3 : (ofArrows w_2 w_3).Extensive
hc : IsColimit (Cofan.mk X w_3)
Y : C
f : Y ⟶ X
h : ofArrows w_2 w_3 f
i : w
⊢ HasPullback f (w_3 i)

Tactic:
apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct hc

Premises used: CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Presieve.{v_1, u_1} X
inst_2 : S.Extensive
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
inst_3 : PreservesFiniteProducts F
obtain :
  ∀ (α : Type),
    Finite α →
      ∀ (Z : α → C) (π : (a : α) → Z a ⟶ X) [(ofArrows Z π).Extensive] (hc : IsColimit (Cofan.mk X π)),
        IsSheafFor F (ofArrows Z π)
⊢ IsSheafFor F S

Tactic:
obtain ⟨α, _, Z, π, rfl, ⟨hc⟩⟩ := Extensive.arrows_nonempty_isColimit (R := S)

Premises used: CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
inst_2 : PreservesFiniteProducts F
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst_3 : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
⊢ (ofArrows Z (Cofan.mk X π).inj).HasPairwisePullbacks

Tactic:
have : (ofArrows Z (Cofan.mk X π).inj).HasPairwisePullbacks :=
    (inferInstance : (ofArrows Z π).HasPairwisePullbacks)
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
inst_2 : PreservesFiniteProducts F
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst_3 : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).HasPairwisePullbacks
intro : ∀ (val : Fintype α), IsSheafFor F (ofArrows Z π)
⊢ IsSheafFor F (ofArrows Z π)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
inst_2 : PreservesFiniteProducts F
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst_3 : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).HasPairwisePullbacks
val : Fintype α
⊢ IsSheafFor F (ofArrows Z π)

Tactic:
isSheafFor_of_preservesProduct F _ hc

Premises used: CategoryTheory.Presieve.isSheafFor_of_preservesProduct, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
inst_2 : PreservesFiniteProducts F
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
inst_3 : (ofArrows Z π).Extensive
hc : IsColimit (Cofan.mk X π)
this : (ofArrows Z (Cofan.mk X π).inj).HasPairwisePullbacks
val : Fintype α
⊢ IsSheafFor F (ofArrows Z π)

Tactic:
exact isSheafFor_of_preservesProduct F _ hc

Premises used: CategoryTheory.Presieve.isSheafFor_of_preservesProduct
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
α : Type
inst_3 : Finite α
Z : α → C
⊢ Extensive.{v_1, u_1} (X := sigmaObj.{0, v_1, u_1} Z) (ofArrows Z fun (i : α) ↦ Sigma.ι Z i)

Tactic:
⟨⟨α, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, ⟨coproductIsCoproduct _⟩⟩⟩

Premises used: CategoryTheory.Presieve.Extensive.mk, CategoryTheory.Limits.Sigma.ι, inferInstance, Nonempty.intro, CategoryTheory.Limits.coproductIsCoproduct, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
W : C
rw :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) R →
      IsSheafFor (Functor.obj yoneda W) R
⊢ IsSheaf.{v_1, v_1, u_1} (extensiveTopology C) (Functor.obj yoneda W)

Tactic:
rw [extensiveTopology, isSheaf_coverage]

Premises used: CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.extensiveTopology
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
W X : C
R : Presieve.{v_1, u_1} X
this :
  ∀ (Y : Type) (α : Finite Y) (Z : Y → C) (π : (a : Y) → Z a ⟶ X) (hR : R = ofArrows Z π)
    (hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)), IsSheafFor (Functor.obj yoneda W) R
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) R →
    IsSheafFor (Functor.obj yoneda W) R

Tactic:
⟨Y, α, Z, π, hR, hi⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
W X : C
R : Presieve.{v_1, u_1} X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
⊢ IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc (Cofan.mk X π).inj)

Tactic:
have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
W X : C
R : Presieve.{v_1, u_1} X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
this : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc (Cofan.mk X π).inj)
⊢ R.Extensive

Tactic:
have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
W X : C
R : Presieve.{v_1, u_1} X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
this_1 : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor (Functor.obj yoneda W) R

Tactic:
isSheafFor_extensive_of_preservesFiniteProducts _ _

Premises used: CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
W X : C
R : Presieve.{v_1, u_1} X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
this_1 : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor (Functor.obj yoneda W) R

Tactic:
exact isSheafFor_extensive_of_preservesFiniteProducts _ _

Premises used: CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
⊢ GrothendieckTopology.Subcanonical.{v_1, u_1} (extensiveTopology C)

Tactic:
GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj

Premises used: CategoryTheory.extensiveTopology.isSheaf_yoneda_obj, CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Tactic:
⟨fun hF ↦ ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩, fun hF ↦ ?_⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.mk, Iff.intro, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
refine_1 :
  ∀ (hF : IsSheaf (extensiveTopology C) F) (n : ℕ) {K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ},
    PreservesLimit K F
refine_2 : ∀ (hF : PreservesFiniteProducts F), IsSheaf (extensiveTopology C) F
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Tactic:
refine ⟨fun hF ↦ ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩, fun hF ↦ ?_⟩