-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
lemma equalizerCondition_iff_isSheaf (F : Cᵒᵖ ⥤ D) [Preregular C]
    [∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f] :
    EqualizerCondition F ↔ Presheaf.IsSheaf (regularTopology C) F

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F →
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
rintro hF X _ ⟨Y, f, rfl, _⟩

Result:
case mp.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
hF : EqualizerCondition F
X Y : C
f : Y ⟶ X
right✝ : EffectiveEpi f
⊢ Nonempty (IsLimit (F.mapCone (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone.op))

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ (∀ ⦃X : C⦄,
      ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))) →
    EqualizerCondition F

Tactic:
intro hF Y X f _

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝² : Preregular C
inst✝¹ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
hF : ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
f : Y ⟶ X
inst✝ : EffectiveEpi f
⊢ SingleEqualizerCondition F f

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝² : Preregular C
inst✝¹ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
hF : ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
f : Y ⟶ X
inst✝ : EffectiveEpi f
⊢ SingleEqualizerCondition F f

Tactic:
exact (equalizerConditionMap_iff_nonempty_isLimit F f).2 (hF _ ⟨_, f, rfl, inferInstance⟩)

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F →
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ (∀ ⦃X : C⦄,
      ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))) →
    EqualizerCondition F

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔ Presheaf.IsSheaf (Coverage.toGrothendieck C (regularCoverage C)) F

Tactic:
rw [Presheaf.isSheaf_iff_isLimit_coverage]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔
    ∀ ⦃X : C⦄, ∀ R ∈ (regularCoverage C).covering X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))

Proof state:
case mp.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
hF : EqualizerCondition F
X Y : C
f : Y ⟶ X
right✝ : EffectiveEpi f
⊢ Nonempty (IsLimit (F.mapCone (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone.op))

Tactic:
exact (equalizerConditionMap_iff_nonempty_isLimit F f).1 (hF f)

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔ Presheaf.IsSheaf (regularTopology C) F

Tactic:
dsimp [regularTopology]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ EqualizerCondition F ↔ Presheaf.IsSheaf (Coverage.toGrothendieck C (regularCoverage C)) F