-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
theorem Presieve.isSheaf_iff_preservesFiniteProducts (F : Cᵒᵖ ⥤ Type w) :
    Presieve.IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Proof state:
case refine_1.refine_3
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
x✝ : PreservesLimit (Discrete.functor fun i => op (Z i)) F :=
  preservesProduct_of_isSheafFor F ?refine_1.refine_1 initialIsInitial (Cofan.mk (∐ Z) (Sigma.ι Z))
    (coproductIsCoproduct Z) (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
    (hF (ofArrows Z fun i => Sigma.ι Z i) ?refine_1.refine_2)
⊢ PreservesLimit K F

Tactic:
exact preservesLimit_of_iso_diagram F i.symm

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝¹ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this✝ : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
this : (Sigma.desc fun i => Sigma.ι Z i) = 𝟙 (∐ Z)
⊢ IsIso (Sigma.desc fun i => Sigma.ι Z i)

Tactic:
rw [this]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝¹ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this✝ : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
this : (Sigma.desc fun i => Sigma.ι Z i) = 𝟙 (∐ Z)
⊢ IsIso (𝟙 (∐ Z))

Proof state:
case refine_1.refine_1.a.refine_1.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
b : Empty
⊢ Sigma.ι Empty.elim b ≫ (Sigma.desc fun a => ⋯.elim a) ≫ default = Sigma.ι Empty.elim b ≫ 𝟙 (∐ Empty.elim)

Tactic:
cases b

Result:
no goals

Proof state:
case refine_1
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
⊢ 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)) ?_)

Result:
case refine_1.refine_3
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
x✝ : PreservesLimit (Discrete.functor fun i => op (Z i)) F :=
  preservesProduct_of_isSheafFor F ?refine_1.refine_1 initialIsInitial (Cofan.mk (∐ Z) (Sigma.ι Z))
    (coproductIsCoproduct Z) (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
    (hF (ofArrows Z fun i => Sigma.ι Z i) ?refine_1.refine_2)
⊢ PreservesLimit K F

case refine_1.refine_1
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
⊢ IsSheafFor F (ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a)

case refine_1.refine_2
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
⊢ (ofArrows Z fun i => Sigma.ι Z i) ∈ (extensiveCoverage C).covering (∐ Z)

Proof state:
case refine_2
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ IsSheaf (extensiveTopology C) F

Tactic:
rw [extensiveTopology, Presieve.isSheaf_coverage]

Result:
case refine_2
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝¹ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this✝ : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
this : (Sigma.desc fun i => Sigma.ι Z i) = 𝟙 (∐ Z)
⊢ IsIso (𝟙 (∐ Z))

Tactic:
infer_instance

Result:
no goals