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

Proof state:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Tactic:
exact isLimitOfPreserves (F.comp (coyoneda.obj ⟨E⟩)) hc

Result:
no goals

Proof state:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Tactic:
rw [Presieve.isSheaf_iff_preservesFiniteProducts] at h

Result:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
constructor

Result:
case mp.val
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ PreservesFiniteProducts F

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

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Proof state:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ (X : Dᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone (F.mapCone c))

Tactic:
intro ⟨E⟩

Result:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : IsSheaf (extensiveTopology C) F
⊢ PreservesFiniteProducts F

Tactic:
rw [IsSheaf] at h

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ PreservesFiniteProducts F

Proof state:
case mp.val
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
apply coyonedaJointlyReflectsLimits

Result:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ (X : Dᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone (F.mapCone c))

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F

Tactic:
intro _ E

Result:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
E : D
⊢ Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
E : D
⊢ PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))

Tactic:
exact ⟨inferInstance⟩

Result:
no goals

Proof state:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Tactic:
specialize h E

Result:
case mp.val.hc
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
E : D
⊢ Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))

Tactic:
rw [Presieve.isSheaf_iff_preservesFiniteProducts]

Result:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
a✝ : PreservesFiniteProducts F
E : D
⊢ PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ IsSheaf (extensiveTopology C) F → PreservesFiniteProducts F

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
D : Type u_2
inst✝² : Category.{u_4, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : IsSheaf (extensiveTopology C) F
⊢ PreservesFiniteProducts F