-- 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_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
⊢ (Sigma.desc fun i => Sigma.ι Z i) = 𝟙 (∐ Z)

Tactic:
ext

Result:
case refine_1.refine_2.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✝ : Fin n
⊢ (Sigma.ι Z b✝ ≫ Sigma.desc fun i => Sigma.ι Z i) = Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)

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ᵒᵖ
⊢ PreservesLimit K F

Tactic:
let Z : Fin n → C := fun i ↦ unop (K.obj ⟨i⟩)

Result:
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 })
⊢ PreservesLimit K F

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 })
⊢ PreservesLimit K F

Tactic:
have : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks :=
  inferInstanceAs (ofArrows Z (Sigma.ι Z)).hasPullbacks

Result:
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
⊢ PreservesLimit K F

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
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R

Tactic:
intro X R ⟨Y, α, Z, π, hR, hi⟩

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 : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
⊢ IsSheafFor F R

Proof state:
case refine_1.refine_1.a
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 Empty.elim fun a => Empty.instIsEmpty.elim a) ∈ (extensiveCoverage C).covering (⊥_ C)

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

Result:
case refine_1.refine_1.a.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
⊢ (Sigma.desc fun a => ⋯.elim a) ≫ default = 𝟙 (∐ Empty.elim)

case refine_1.refine_1.a.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
⊢ (default ≫ Sigma.desc fun a => ⋯.elim a) = 𝟙 (⊥_ C)

Proof state:
case refine_1.refine_2.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✝ : Fin n
⊢ (Sigma.ι Z b✝ ≫ Sigma.desc fun i => Sigma.ι Z i) = Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)

Tactic:
simp

Result:
no goals

Proof state:
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)

Tactic:
apply hF

Result:
case refine_1.refine_1.a
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 Empty.elim fun a => Empty.instIsEmpty.elim a) ∈ (extensiveCoverage C).covering (⊥_ C)