Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_1.refine_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings 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).HasPairwisePullbacks
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

pp: case refine_1.refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings 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).HasPairwisePullbacks
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)

pp: case refine_1.refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings 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).HasPairwisePullbacks
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).coverings (∐ Z)

Tactic:
· exact preservesLimit_of_iso_diagram F i.symm

Goal state after:
case refine_1.refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings 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).HasPairwisePullbacks
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.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings 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).HasPairwisePullbacks
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).coverings (∐ Z)