awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i : α
⊢ S.arrows (π i)

Tactic:
h' _
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i : α
⊢ S.arrows (π i)

Tactic:
exact h' _
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

Tactic:
exact fun _ _ hh ↦ by cases hh; exact h' _
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) (Presieve.ofArrows Y π)

Tactic:
⟨α, inferInstance, Y, π, rfl, ?_⟩

Premises used: Set.Mem, setOf, inferInstance, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
mpr : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) (Presieve.ofArrows Y π)

Tactic:
refine ⟨α, inferInstance, Y, π, rfl, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
mpr : Nonempty (IsColimit (Cofan.mk X π))
⊢ IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)

Tactic:
rw [← show _ ↔ IsIso (Sigma.desc π) from
        Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc (c := Cofan.mk X π)]

Premises used: CategoryTheory.Limits.Cofan.mk, CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
h
-- Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
mp :
  Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f →
    ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
      ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
        ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))
mpr :
  (∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
      ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
        ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))) →
    Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f ↔
    ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
      ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
        ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ {U : C} (s : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))),
    Presheaf.imageSieve (FA := FD) (CA := CD) f s ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
⊢ Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) X

Tactic:
specialize h y
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
h : Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π

Tactic:
rw [regularTopology.mem_sieves_iff_hasEffectiveEpi] at h

Premises used: CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
h : ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
mp :
  ∀ (X' : C) (π : X' ⟶ X) (h : EffectiveEpi π) (h' : (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))

Tactic:
obtain ⟨X', π, h, h'⟩ := h
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
X' : C
π : X' ⟶ X
h : EffectiveEpi π
h' : (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))

Tactic:
⟨X', π, h, h'⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
X : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))
X' : C
π : X' ⟶ X
h : EffectiveEpi π
h' : (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))

Tactic:
exact ⟨X', π, h, h'⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f

Tactic:
⟨fun y ↦ ?_⟩

Premises used: CategoryTheory.Presheaf.IsLocallySurjective.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
mpr :
  ∀ {U : C} (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))),
    Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
⊢ Presheaf.IsLocallySurjective (regularTopology C) (FA := FD) (CA := CD) f

Tactic:
refine ⟨fun y ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
U : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))
mpr :
  ∀ (X' : C) (π : X' ⟶ U) (h : EffectiveEpi π)
    (h' :
      ∃ (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
        Eq (α := CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
              x :
            CD (G.obj (op X')))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op π)) : (a : CD (G.obj (op U))) → CD (G.obj (op X')))
              y :
            CD (G.obj (op X')))),
    Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
⊢ Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U

Tactic:
obtain ⟨X', π, h, h'⟩ := h _ y
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h_1 :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
U : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))
X' : C
π : X' ⟶ U
h : EffectiveEpi π
h' :
  ∃ (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op π)) : (a : CD (G.obj (op U))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
mpr : ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π
⊢ Presheaf.imageSieve (FA := FD) (CA := CD) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U

Tactic:
rw [regularTopology.mem_sieves_iff_hasEffectiveEpi]

Premises used: CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h_1 :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
U : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))
X' : C
π : X' ⟶ U
h : EffectiveEpi π
h' :
  ∃ (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op π)) : (a : CD (G.obj (op U))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
⊢ ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π

Tactic:
⟨X', π, h, h'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_2, u_2, u_3} D FD (CC := CD)
inst_4 : Preregular.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
h_1 :
  ∀ (X : C) (y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
      Eq (α := CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X')))
            x :
          CD (G.obj (op X')))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op φ)) : (a : CD (G.obj (op X))) → CD (G.obj (op X'))) y :
          CD (G.obj (op X')))
U : C
y : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (G.obj (op U))
X' : C
π : X' ⟶ U
h : EffectiveEpi π
h' :
  ∃ (x : ToType.{w, v_2, u_2, u_3} (FC := FD) (CC := CD) (F.obj (op X'))),
    Eq (α := CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (f.app (op X')) : (a : CD (F.obj (op X'))) → CD (G.obj (op X'))) x :
        CD (G.obj (op X')))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map (op π)) : (a : CD (G.obj (op U))) → CD (G.obj (op X'))) y :
        CD (G.obj (op X')))
⊢ ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := FD) (CA := CD) f y).arrows π

Tactic:
exact ⟨X', π, h, h'⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (extensiveTopology C) (FA := TypeCat.Fun) f
X : C
x : G.obj (op X)
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f x ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X

Tactic:
replace h := h.1 x
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h : Presheaf.imageSieve (FA := TypeCat.Fun) f x ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)

Tactic:
rw [mem_sieves_iff_contains_colimit_cofan] at h

Premises used: CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_2 : PreservesFiniteProducts F
inst_3 : PreservesFiniteProducts G
X : C
x : G.obj (op X)
h :
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
obtain :
  ∀ (α : Type),
    Finite α →
      ∀ (Y : α → C) (π : (a : α) → Y a ⟶ X) (h : Nonempty (IsColimit (Cofan.mk X π)))
        (h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)),
        ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
                (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
              a =
            x
⊢ ∃ (a : (fun (X : Type w) ↦ X) (F.obj (op X))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op X)))
        a =
      x

Tactic:
obtain ⟨α, _, Y, π, h, h'⟩ := h