awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hF : IsSheaf (extensiveTopology C) F
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
refine_1 :
  ∀
    (hF :
      ∀ {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 F R)
    (n : ℕ) {K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ}, PreservesLimit K F
⊢ PreservesLimit K F

Tactic:
rw [extensiveTopology, isSheaf_coverage] at hF

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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
⊢ ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)

Tactic:
have : ∀ (i : Fin n), Mono (Cofan.inj (Cofan.mk (∐ Z) (Sigma.ι Z)) i) :=
      inferInstanceAs <| ∀ (i : Fin n), Mono (Sigma.ι Z i)
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
refine_1 : PreservesLimit K F
refine_1₁ :
  IsSheafFor (X := initial.{v_1, u_1} C) F
    (ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a)
refine_1₂ :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} Z)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) (sigmaObj.{0, v_1, u_1} Z))
    (ofArrows Z fun (i : Fin n) ↦ Sigma.ι Z i)
⊢ PreservesLimit K F

Tactic:
let _ : PreservesLimit (Discrete.functor (fun i ↦ op (Z i))) F :=
        Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial _ (coproductIsCoproduct Z)
        (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
        (hF (Presieve.ofArrows Z (fun i ↦ Sigma.ι Z i)) ?_)
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
h : PreservesLimit (J := Discrete (Fin n)) (Discrete.functor fun (i : Fin n) ↦ op (Z i)) F := ⋯
⊢ PreservesLimit K F

Tactic:
preservesLimit_of_iso_diagram F i.symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
h : PreservesLimit (J := Discrete (Fin n)) (Discrete.functor fun (i : Fin n) ↦ op (Z i)) F := ⋯
⊢ PreservesLimit K F

Tactic:
exact preservesLimit_of_iso_diagram F i.symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
refine_1 :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} (initial.{v_1, u_1} C)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) (initial.{v_1, u_1} C))
    (ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a)
⊢ IsSheafFor (X := initial.{v_1, u_1} C) F
    (ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a)

Tactic:
apply hF
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (initial.{v_1, u_1} C)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) (initial.{v_1, u_1} C))
    (ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a)

Tactic:
⟨Empty, inferInstance, Empty.elim, IsEmpty.elim inferInstance, rfl, ⟨default,?_, ?_⟩⟩

Premises used: Inhabited.default, Empty.elim, Set.Mem, IsEmpty.elim, setOf, inferInstance, Empty, And.intro, Exists.intro, CategoryTheory.IsIso.mk, 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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
refine_1 :
  Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C) (sigmaObj.{0, v_1, u_1} Empty.elim) (sigmaObj.{0, v_1, u_1} Empty.elim))
    (CategoryStruct.comp (Y := initial.{v_1, u_1} C)
      (Sigma.desc fun (a : Empty) ↦ IsEmpty.elim ⋯ (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a) default)
    (𝟙 (sigmaObj.{0, v_1, u_1} Empty.elim))
refine_1₁ :
  Eq.{v_1 + 1} (α := initial.{v_1, u_1} C ⟶ initial.{v_1, u_1} C)
    (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} Empty.elim) default
      (Sigma.desc fun (a : Empty) ↦ IsEmpty.elim ⋯ (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a))
    (𝟙 (initial.{v_1, u_1} C))
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (initial.{v_1, u_1} C)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) (initial.{v_1, u_1} C))
    (ofArrows Empty.elim fun (a : Empty) ↦
      Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a)

Tactic:
refine ⟨Empty, inferInstance, Empty.elim, IsEmpty.elim inferInstance, rfl, ⟨default,?_, ?_⟩⟩
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
refine_1 :
  ∀ (b : Empty),
    Eq.{v_1 + 1} (α := Quiver.Hom.{v_1, u_1} (V := C) b.elim (sigmaObj.{0, v_1, u_1} Empty.elim))
      (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} Empty.elim) (Sigma.ι Empty.elim b)
        (CategoryStruct.comp (Y := initial.{v_1, u_1} C)
          (Sigma.desc fun (a : Empty) ↦ IsEmpty.elim ⋯ (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a)
          default))
      (Sigma.ι Empty.elim b ≫ 𝟙 (sigmaObj.{0, v_1, u_1} Empty.elim))
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C) (sigmaObj.{0, v_1, u_1} Empty.elim) (sigmaObj.{0, v_1, u_1} Empty.elim))
    (CategoryStruct.comp (Y := initial.{v_1, u_1} C)
      (Sigma.desc fun (a : Empty) ↦ IsEmpty.elim ⋯ (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a) default)
    (𝟙 (sigmaObj.{0, v_1, u_1} Empty.elim))

Tactic:
ext b
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
b : Empty
⊢ Eq.{v_1 + 1} (α := Quiver.Hom.{v_1, u_1} (V := C) b.elim (sigmaObj.{0, v_1, u_1} Empty.elim))
    (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} Empty.elim) (Sigma.ι Empty.elim b)
      (CategoryStruct.comp (Y := initial.{v_1, u_1} C)
        (Sigma.desc fun (a : Empty) ↦ IsEmpty.elim ⋯ (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a) default))
    (Sigma.ι Empty.elim b ≫ 𝟙 (sigmaObj.{0, v_1, u_1} Empty.elim))

Tactic:
cases b
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
⊢ Eq.{v_1 + 1} (α := initial.{v_1, u_1} C ⟶ initial.{v_1, u_1} C)
    (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} Empty.elim) default
      (Sigma.desc fun (a : Empty) ↦ IsEmpty.elim ⋯ (p := fun (x : Empty) ↦ x.elim ⟶ initial.{v_1, u_1} C) a))
    (𝟙 (initial.{v_1, u_1} C))

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} Z)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) (sigmaObj.{0, v_1, u_1} Z))
    (ofArrows Z fun (i : Fin n) ↦ Sigma.ι Z i)

Tactic:
⟨Fin n, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, instIsIsoDescι⟩

Premises used: Set.Mem, setOf, CategoryTheory.Limits.Sigma.ι, inferInstance, And.intro, Exists.intro, CategoryTheory.Limits.instIsIsoDescι, Fin, 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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF :
  ∀ {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 F R
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
Z : Fin n → C := fun (i : Fin n) ↦ unop (K.obj { as := i })
this_1 : (ofArrows Z (Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj).HasPairwisePullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (sigmaObj.{0, v_1, u_1} Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun (i : Fin n) ↦ op (Z i) := Discrete.natIsoFunctor
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} (sigmaObj.{0, v_1, u_1} Z)))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) (sigmaObj.{0, v_1, u_1} Z))
    (ofArrows Z fun (i : Fin n) ↦ Sigma.ι Z i)

Tactic:
exact ⟨Fin n, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, instIsIsoDescι⟩
-- 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)
hF : PreservesFiniteProducts F
refine_2 :
  ∀ {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 F R
⊢ IsSheaf (extensiveTopology C) F

Tactic:
rw [extensiveTopology, Presieve.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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
X : C
R : Presieve.{v_1, u_1} X
refine_2 :
  ∀ (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 F R
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) R →
    IsSheafFor F 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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
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 F R

Tactic:
isSheafFor_extensive_of_preservesFiniteProducts R F

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
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
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 F R

Tactic:
exact isSheafFor_extensive_of_preservesFiniteProducts R F

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
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
mp : IsSheaf (extensiveTopology C) F → PreservesFiniteProducts F
mpr : PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Tactic:
constructor
-- 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
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : IsSheaf (extensiveTopology C) F
⊢ ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))

Tactic:
rw [IsSheaf] at h

Premises used: CategoryTheory.Presheaf.IsSheaf
-- 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
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
⊢ PreservesFiniteProducts F

Tactic:
⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesLimit.mk, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- 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
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
mp :
  ∀ (n : ℕ) {K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ} {c : Cone K} (hc : IsLimit c),
    Nonempty (IsLimit (F.mapCone c))
⊢ PreservesFiniteProducts F

Tactic:
refine ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
-- 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
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
mp : IsLimit (F.mapCone c)
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
constructor
-- 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
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
mp :
  (X : Dᵒᵖ) → IsLimit (F := (K ⋙ F) ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) (F.mapCone c))
⊢ IsLimit (F.mapCone c)

Tactic:
apply coyonedaJointlyReflectsLimits

Premises used: CategoryTheory.coyonedaJointlyReflectsLimits