awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Y a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            x :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
ht : IsLimit (J := Discrete α) (F := Discrete.functor fun (a : α) ↦ F.obj (op (Y a)))
  (LimitCone.cone (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))) :=
  LimitCone.isLimit (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  ((Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm :
      (a : IsLimit (Cocone.op (Cofan.mk X π))) →
        IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))))
    h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht')
    (Discrete.natIso fun (x : Discrete α) ↦ Iso.refl (F.obj (op (Y x.as))))
⊢ ∃ (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:
⟨i.hom y, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Exists.intro, CategoryTheory.Iso.hom, DFunLike.coe
-- 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)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Y a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Y a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op X))) → (fun (X : Type w) ↦ X) (G.obj (op (Y a))))
            x :
          (fun (X : Type w) ↦ X) (G.obj (op (Y a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
ht : IsLimit (J := Discrete α) (F := Discrete.functor fun (a : α) ↦ F.obj (op (Y a)))
  (LimitCone.cone (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))) :=
  LimitCone.isLimit (Types.productLimitCone fun (a : α) ↦ F.obj (op (Y a)))
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  ((Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm :
      (a : IsLimit (Cocone.op (Cofan.mk X π))) →
        IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))))
    h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht')
    (Discrete.natIso fun (x : Discrete α) ↦ Iso.refl (F.obj (op (Y x.as))))
refine :
  (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)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) i.hom :
            (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Y a)))) → (fun (X : Type w) ↦ X) (F.obj (op X)))
          y :
        (fun (X : Type w) ↦ X) (F.obj (op X))) =
    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:
refine ⟨i.hom 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 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
mp :
  Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))
mpr :
  (∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f ↔
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))

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 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
mp :
  Presheaf.IsLocallySurjective (extensiveTopology C) (FA := TypeCat.Fun)
      (Functor.whiskerRight f (forget D (FC := FD) (CC := CD))) →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget (J := extensiveTopology C)]

Premises used: CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.extensiveTopology
-- 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 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := TypeCat.Fun)
      (Functor.whiskerRight f (forget D (FC := FD) (CC := CD))) →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))

Tactic:
fun h _ ↦
      surjective_of_isLocallySurjective_sheaf_of_types (Functor.whiskerRight f (forget D)) h

Premises used: CategoryTheory.Functor.whiskerRight, CategoryTheory.forget, CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types
-- 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 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (FA := TypeCat.Fun)
      (Functor.whiskerRight f (forget D (FC := FD) (CC := CD))) →
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))

Tactic:
exact fun h _ ↦
      surjective_of_isLocallySurjective_sheaf_of_types (Functor.whiskerRight f (forget D)) h

Premises used: CategoryTheory.Functor.whiskerRight, CategoryTheory.forget, CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types
-- 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 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ (∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f

Tactic:
fun a ↦
      Presheaf.isLocallySurjective_of_surjective _ _ (fun _ ↦ a _)

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_surjective, Opposite.unop, CategoryTheory.extensiveTopology
-- 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 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
f : F ⟶ G
inst_5 : PreservesFiniteProducts F
inst_6 : PreservesFiniteProducts G
inst_7 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ (∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (op X))) (β := 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)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) (FA := FD) (CA := CD) f

Tactic:
exact fun a ↦
      Presheaf.isLocallySurjective_of_surjective _ _ (fun _ ↦ a _)

Premises used: CategoryTheory.Presheaf.isLocallySurjective_of_surjective
-- 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 : FinitaryExtensive.{v_1, u_1} C
F G : Sheaf.{v_1, v_2, u_1, u_2} (extensiveTopology C) D
f : F ⟶ G
inst_5 : PreservesFiniteProducts.{v_2, w, u_2, w + 1} (forget D (FC := FD) (CC := CD))
⊢ IsLocallySurjective (FA := FD) (CA := CD) f ↔
    ∀ (X : C),
      Function.Surjective.{w + 1, w + 1} (α := CD (F.obj (P := Presheaf.IsSheaf (extensiveTopology C)).obj (op X)))
        (β := CD (G.obj (P := Presheaf.IsSheaf (extensiveTopology C)).obj (op X)))
        (⇑(ConcreteCategory.hom (FC := FD) (CC := CD) (f.hom.app (op X))) :
          (a : CD (F.obj.obj (op X))) → CD (G.obj.obj (op X)))

Tactic:
extensiveTopology.presheafIsLocallySurjective_iff _ f.hom

Premises used: CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (coherentTopology C) (FA := TypeCat.Fun) f
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (coherentTopology C : (a : C) → Set (Sieve a)) U

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

Tactic:
rw [coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily] at h

Premises used: CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
h :
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ U),
    EffectiveEpiFamily Y π ∧ ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
obtain :
  ∀ (α : Type),
    Finite α →
      ∀ (Z : α → C) (π : (a : α) → Z a ⟶ U) (h : EffectiveEpiFamily Z π)
        (h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)),
        Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U

Tactic:
obtain ⟨α, _, Z, π, h, h'⟩ := h
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
rw : ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows π
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f y ∈ (regularTopology C : (a : C) → Set (Sieve a)) U

Tactic:
rw [mem_sieves_iff_hasEffectiveEpi]

Premises used: CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Z a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (sigmaObj.{0, v_1, u_1} Z)) :=
  Iso.symm (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≪≫
    Iso.symm (PreservesProduct.iso F fun (a : α) ↦ op (Z a)) ≪≫ F.mapIso (Iso.symm (opCoproductIsoProduct Z))
⊢ ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows π

Tactic:
⟨∐ Z, Sigma.desc π, inferInstance, i'.hom x, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, And.intro, Exists.intro, CategoryTheory.Limits.Sigma.desc, CategoryTheory.Limits.sigmaObj, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Z a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (sigmaObj.{0, v_1, u_1} Z)) :=
  Iso.symm (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≪≫
    Iso.symm (PreservesProduct.iso F fun (a : α) ↦ op (Z a)) ≪≫ F.mapIso (Iso.symm (opCoproductIsoProduct Z))
refine :
  Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (sigmaObj.{0, v_1, u_1} Z))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (∐ Z)))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) i'.hom :
              (a : (fun (X : Type w) ↦ X) ((a : α) → F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (F.obj (op (∐ Z))))
            x :
          (fun (X : Type w) ↦ X) (F.obj (op (sigmaObj.{0, v_1, u_1} Z)))) :
      (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (Quiver.Hom.op (Sigma.desc π))) :
          (a : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (∐ Z))))
        y :
      (fun (X : Type w) ↦ X) (G.obj (op (sigmaObj.{0, v_1, u_1} Z))))
⊢ ∃ (Y : C) (π : Y ⟶ U), EffectiveEpi π ∧ (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows π

Tactic:
refine ⟨∐ Z, Sigma.desc π, inferInstance, i'.hom x, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
F G : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
f : F ⟶ G
inst_3 : PreservesFiniteProducts F
inst_4 : PreservesFiniteProducts G
U : C
y : ToType (FC := TypeCat.Fun) (G.obj (op U))
α : Type
w : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve (FA := TypeCat.Fun) f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) :=
  fun (a : α) ↦
    Exists.choose (p := fun (t : ToType (FC := TypeCat.Fun) (F.obj (op (Z a)))) ↦
      Eq (α := (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (Z a))) :
              (a_1 : (fun (X : Type w) ↦ X) (F.obj (op (Z a)))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            t :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (π a).op) :
              (a_1 : (fun (X : Type w) ↦ X) (G.obj (op U))) → (fun (X : Type w) ↦ X) (G.obj (op (Z a))))
            y :
          (fun (X : Type w) ↦ X) (G.obj (op (Z a)))))
      ⋯
x_1 : Fintype α := Fintype.ofFinite α
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (sigmaObj.{0, v_1, u_1} Z)) :=
  Iso.symm (Types.productIso fun (a : α) ↦ F.obj (op (Z a))) ≪≫
    Iso.symm (PreservesProduct.iso F fun (a : α) ↦ op (Z a)) ≪≫ F.mapIso (Iso.symm (opCoproductIsoProduct Z))
⊢ PreservesLimitsOfShape (Discrete α)ᵒᵖ G

Tactic:
have := preservesLimitsOfShape_of_equiv (Discrete.opposite α).symm G