mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
X : C
y : ToType (G.obj (op X))
h : ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y

Tactic:
]

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
X : C
y : ToType (G.obj (op X))
h : ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
X : C
y : ToType (G.obj (op X))
h : Presheaf.imageSieve f y ∈ (regularTopology C) X
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y

Tactic:
rw [regularTopology.mem_sieves_iff_hasEffectiveEpi] at h

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
X : C
y : ToType (G.obj (op X))
h : ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)

Tactic:
]

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
h✝ :
  ∀ (X : C) (y : ToType (G.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
U✝ : C
y : ToType (G.obj (op U✝))
X' : C
π : X' ⟶ U✝
h : EffectiveEpi π
h' : ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op π))) y
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π

Tactic:
]

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
h✝ :
  ∀ (X : C) (y : ToType (G.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
U✝ : C
y : ToType (G.obj (op U✝))
X' : C
π : X' ⟶ U✝
h : EffectiveEpi π
h' : ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op π))) y
⊢ ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝³ : IsLocallySurjective data.i
this✝² : IsLocallyInjective data.p
this✝¹ : Epi data.p
this✝ : Mono data.p
this : IsIso data.p
⊢ IsLocallySurjective (data.i ≫ data.p)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝³ : IsLocallySurjective data.i
this✝² : IsLocallyInjective data.p
this✝¹ : Epi data.p
this✝ : Mono data.p
this : IsIso data.p
⊢ IsLocallySurjective (data.i ≫ data.p)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
]

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h :
  ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
⊢ ∃ a, (ConcreteCategory.hom (f.app (op X))) a = x

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h :
  ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
⊢ ∃ a, (ConcreteCategory.hom (f.app (op X))) a = x
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))

Tactic:
]

Goal state after:
case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ S.arrows (F.preimage (g₀ ≫ g₂ ≫ F.map g₁))
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ ∃ Y π, EffectiveEpi π ∧ S.arrows π
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
this : Preregular C
⊢ S ∈ (regularTopology C) X ↔ S ∈ (regularTopology C) X

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
exact isSheaf_sup (extensiveCoverage C) (regularCoverage C) F

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ PreservesFiniteProducts F ↔ PreservesFiniteProducts F

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, 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) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, 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) [EffectiveEpi f], HasPullback f f
inst✝ : PreservesFiniteLimits s
hF : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (f.app (op (Y a)))) ((ConcreteCategory.hom (F.map (π a).op)) ((ConcreteCategory.hom i.hom) y)) =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom (f.app (op (Y a)))) ((ConcreteCategory.hom (F.map (π a).op)) ((ConcreteCategory.hom i.hom) y)) =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, 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) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, 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) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
hF : PreservesFiniteProducts (F ⋙ s) ∧ EqualizerCondition (F ⋙ s)
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, 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
inst✝¹ : ∀ (X : C), Projective X
inst✝ : PreservesFiniteProducts s
hF : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, 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
inst✝¹ : ∀ (X : C), Projective X
inst✝ : PreservesFiniteProducts s
hF : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, 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
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, 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
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        (((Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone.π.app { as := a } ≫
            (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a }) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        (((Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone.π.app { as := a } ≫
            (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a }) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv =
    equalizer.lift (P.map π.op) ⋯

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).inv =
    equalizer.lift (P.map π.op) ⋯
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (Functor.whiskerRight f (forget D)) →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

Tactic:
]

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁴ : ConcreteCategory D FD
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (Functor.whiskerRight f (forget D)) →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ EqualizerCondition P →
    ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
intro hP

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
⊢ ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)