-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveColimits.lean
lemma isSheaf_pointwiseColimit [PreservesFiniteProducts (colim (J := J) (C := A))]
    (G : J ⥤ Sheaf (extensiveTopology C) A) :
    Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf _ A)).pt

Proof state:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)

Tactic:
apply (config := { allowSynthFailures := true } ) comp_preservesFiniteProducts

Result:
case inst
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip

Proof state:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Tactic:
dsimp only [pointwiseCocone_pt]

Result:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).flip ⋙ colim)

Proof state:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
i : J
⊢ PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]

Result:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
i : J
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Proof state:
case inst
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
this : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip

Tactic:
exact ⟨fun _ ↦ preservesLimitsOfShape_of_evaluation _ _ fun d ↦
  inferInstanceAs (PreservesLimitsOfShape _ ((G ⋙ sheafToPresheaf _ _).obj d))⟩

Result:
no goals

Proof state:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Tactic:
rw [Presheaf.isSheaf_iff_preservesFiniteProducts]

Result:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Proof state:
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
i : J
⊢ Presheaf.IsSheaf (extensiveTopology C) ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)

Tactic:
exact Sheaf.cond _

Result:
no goals

Proof state:
case inst
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip

Tactic:
have : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf _ A).obj i) := fun i ↦ by
  rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]
  exact Sheaf.cond _

Result:
case inst
A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{u_4, u_1} A
inst✝⁴ : Category.{u_6, u_2} C
inst✝³ : Category.{u_5, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
this : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf (extensiveTopology C) A).obj i)
⊢ PreservesFiniteProducts (G ⋙ sheafToPresheaf (extensiveTopology C) A).flip