-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
lemma isSheaf_coherent_of_hasPullbacks_of_comp [Preregular C] [FinitaryExtensive C]
    [h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f]
    [ReflectsFiniteLimits s]
    (hF : IsSheaf (coherentTopology C) (F ⋙ s)) : IsSheaf (coherentTopology C) F

Proof state:
case intro.refine_2
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
x✝² x✝¹ : C
π : x✝² ⟶ x✝¹
x✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (F.map π.op) ⋯)

Tactic:
exact isLimitOfIsLimitForkMap s _ (hF₂ π c hc).some

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
obtain ⟨_, hF₂⟩ := hF

Result:
case intro
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Proof state:
case intro.refine_1
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
exact ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩

Result:
no goals

Proof state:
case intro
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

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

Result:
case intro.refine_1
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

case intro.refine_2
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
x✝² x✝¹ : C
π : x✝² ⟶ x✝¹
x✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (F.map π.op) ⋯)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition (h := h)] at hF ⊢

Result:
C : Type u_1
inst✝⁵ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F