awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF : EqualizerCondition F
X Y : C
f : Y ⟶ X
right : EffectiveEpi f
⊢ Nonempty
    (IsLimit (J :=
      (Presieve.category.{v_1, u_1} (C := C) (X := X)
          (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))))ᵒᵖ)
      (F.mapCone
        (Cocone.op (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))))))

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

Premises used: CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF :
  ∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
      Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
f : Y ⟶ X
mpr : ∀ [EffectiveEpi f], SingleEqualizerCondition F f
⊢ ∀ [EffectiveEpi f], SingleEqualizerCondition F f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF :
  ∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
      Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
f : Y ⟶ X
inst_4 : EffectiveEpi f
⊢ SingleEqualizerCondition F f

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

Premises used: Iff.mpr, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, inferInstance, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
hF :
  ∀ ⦃X : C⦄ (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
      Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))
Y X : C
f : Y ⟶ X
inst_4 : EffectiveEpi f
⊢ SingleEqualizerCondition F f

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

Premises used: Iff.mpr, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, inferInstance, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
S : Presieve.{v_1, u_1} X
inst_1 : S.regular
inst_2 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
obtain :
  ∀ (Y : C) (f : Y ⟶ X) (hf : EffectiveEpi f)
    [regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)],
    IsSheafFor (X := X) F (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
⊢ IsSheafFor F S

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := Presieve.regular.single_epi (R := S)

Premises used: CategoryTheory.Presieve.regular.single_epi, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
inst_1 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst_2 : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
rw :
  ∀ (x : (i : Unit) → F.obj (op Y)),
    Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x →
      ∃! t : (fun (X : Type u_4) ↦ X) (F.obj (op X)),
        ∀ (i : Unit),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
              t =
            x i
⊢ IsSheafFor (X := X) F (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)

Tactic:
rw [isSheafFor_arrows_iff]

Premises used: CategoryTheory.Presieve.isSheafFor_arrows_iff
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
inst_1 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst_2 : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
⊢ ∀ (x : (i : Unit) → F.obj (op Y)),
    Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x →
      ∃! t : (fun (X : Type u_4) ↦ X) (F.obj (op X)),
        ∀ (i : Unit),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
              t =
            x i

Tactic:
fun x hx ↦ ⟨F.map (Projective.factorThru (𝟙 _) f).op <| x (), fun _ ↦ ?_, fun y h ↦ ?_⟩

Premises used: Unit.unit, CategoryTheory.Projective.factorThru, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, ExistsUnique, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
inst_1 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst_2 : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
refine_1 :
  ∀ (x : (i : Unit) → F.obj (op Y)) (hx : Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x) (x_1 : Unit),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Projective.factorThru (𝟙 X) f).op) :
              (a : (fun (X : Type u_4) ↦ X) (F.obj (op Y))) → (fun (X : Type u_4) ↦ X) (F.obj (op X)))
            (x ()) :
          (fun (X : Type u_4) ↦ X) (F.obj (op X))) =
      x x_1
refine_2 :
  ∀ (x : (i : Unit) → F.obj (op Y)) (hx : Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x)
    (y : (fun (X : Type u_4) ↦ X) (F.obj (op X)))
    (h :
      (fun (t : (fun (X : Type u_4) ↦ X) (F.obj (op X))) ↦
          ∀ (i : Unit),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                  (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
                t =
              x i)
        y),
    y =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Projective.factorThru (𝟙 X) f).op) :
          (a : (fun (X : Type u_4) ↦ X) (F.obj (op Y))) → (fun (X : Type u_4) ↦ X) (F.obj (op X)))
        (x ())
⊢ ∀ (x : (i : Unit) → F.obj (op Y)),
    Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x →
      ∃! t : (fun (X : Type u_4) ↦ X) (F.obj (op X)),
        ∀ (i : Unit),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
              t =
            x i

Tactic:
refine fun x hx ↦ ⟨F.map (Projective.factorThru (𝟙 _) f).op <| x (), fun _ ↦ ?_, fun y h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
inst_1 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst_2 : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x : (i : Unit) → F.obj (op Y)
hx : Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x
x_1 : Unit
⊢ Eq (α := Y ⟶ X) (𝟙 Y ≫ (fun (x : Unit) ↦ f) ()) ((f ≫ Projective.factorThru (𝟙 X) f) ≫ (fun (x : Unit) ↦ f) ())

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
inst_1 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst_2 : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x : (i : Unit) → F.obj (op Y)
hx : Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x
x_1 : Unit
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Projective.factorThru (𝟙 X) f).op) :
            (a : (fun (X : Type u_4) ↦ X) (F.obj (op Y))) → (fun (X : Type u_4) ↦ X) (F.obj (op X)))
          (x ()) :
        (fun (X : Type u_4) ↦ X) (F.obj (op X))) =
    x x_1

Tactic:
simpa using (hx () () Y (𝟙 Y) (f ≫ (Projective.factorThru (𝟙 _) f)) (by simp)).symm

Premises used: Unit.unit, CategoryTheory.Projective.factorThru, CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
inst_1 : Projective.{v_1, u_1} X
F : Functor.{v_1, u_4, u_1, u_4 + 1} Cᵒᵖ (Type u_4)
Y : C
f : Y ⟶ X
hf : EffectiveEpi f
inst_2 : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x : (i : Unit) → F.obj (op Y)
hx : Arrows.Compatible F (B := X) (fun (x : Unit) ↦ f) x
y : (fun (X : Type u_4) ↦ X) (F.obj (op X))
h :
  (fun (t : (fun (X : Type u_4) ↦ X) (F.obj (op X))) ↦
      ∀ (i : Unit),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type u_4) ↦ X) (F.obj (op X))) → (fun (X : Type u_4) ↦ X) (F.obj (op Y)))
            t =
          x i)
    y
⊢ y =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Projective.factorThru (𝟙 X) f).op) :
        (a : (fun (X : Type u_4) ↦ X) (F.obj (op Y))) → (fun (X : Type u_4) ↦ X) (F.obj (op X)))
      (x ())

Tactic:
simp [← h (), ← comp_apply, ← Functor.map_comp, ← op_comp]

Premises used: Unit.unit, CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : Preregular.{v_1, u_1} C
inst_3 : ∀ (X : C), Projective.{v_1, u_1} X
⊢ Presheaf.IsSheaf (regularTopology C) F

Tactic:
fun _ ↦ (isSheaf_coverage _ _).mpr fun S ⟨_, h⟩ ↦ have : S.regular := ⟨_, h⟩
    isSheafFor_regular_of_projective _ _

Premises used: CategoryTheory.regularTopology.isSheafFor_regular_of_projective, Iff.mpr, CategoryTheory.coyoneda, CategoryTheory.regularCoverage, CategoryTheory.Presieve.IsSheafFor, CategoryTheory.Functor.comp, _private.0.CategoryTheory.regularTopology.isSheaf_of_projective.match_1, CategoryTheory.regularTopology, Opposite.op, CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.Presieve.regular.mk, Exists.intro, CategoryTheory.Presheaf.IsSheaf, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W : C
rw :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) R →
      IsSheafFor (obj yoneda W) R
⊢ IsSheaf.{v_1, v_1, u_1} (regularTopology C) (obj yoneda W)

Tactic:
rw [regularTopology, isSheaf_coverage]

Premises used: CategoryTheory.regularTopology, CategoryTheory.Presieve.isSheaf_coverage
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X : C
S : Presieve.{v_1, u_1} X
this :
  ∀ (w : C) (hS : ∃ (f : w ⟶ X), (S = ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f) ∧ EffectiveEpi f),
    IsSheafFor (obj yoneda W) S
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X) S →
    IsSheafFor (obj yoneda W) S

Tactic:
⟨_, hS⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X : C
S : Presieve.{v_1, u_1} X
w : C
hS : ∃ (f : w ⟶ X), (S = ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f) ∧ EffectiveEpi f
⊢ S.regular

Tactic:
have : S.regular := ⟨_, hS⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X : C
S : Presieve.{v_1, u_1} X
w : C
hS : ∃ (f : w ⟶ X), (S = ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f) ∧ EffectiveEpi f
this : S.regular
obtain :
  ∀ (Y : C) (f : Y ⟶ X) (hf : EffectiveEpi f)
    (hS :
      ∃ (f_1 : w ⟶ X),
        Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
            (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
          EffectiveEpi f_1)
    (this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)),
    IsSheafFor.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
⊢ IsSheafFor (obj yoneda W) S

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := Presieve.regular.single_epi (R := S)

Premises used: CategoryTheory.Presieve.regular.single_epi, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
have :
  ∀ (h_colim : IsColimit (Sieve.generateSingleton f).arrows.cocone),
    IsSheafFor.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
⊢ IsSheafFor.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)

Tactic:
have h_colim := isColimitOfEffectiveEpiStruct f hf.effectiveEpi.some
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim : IsColimit (Sieve.generateSingleton f).arrows.cocone
rw :
  ∀
    (h_colim :
      IsColimit (J :=
        Presieve.category.{v_1, u_1} (C := C) (X := X)
          (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
        (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))),
    IsSheafFor.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
⊢ IsSheafFor.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)

Tactic:
rw [← Sieve.generateSingleton_eq, ← Presieve.ofArrows_pUnit] at h_colim

Premises used: CategoryTheory.Sieve.generateSingleton_eq, CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
⊢ x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))

Tactic:
have hx_ext := Presieve.FamilyOfElements.Compatible.sieveExtend hx
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
obtain :
  ∀ (t : obj (obj yoneda W) (op X)) (t_amalg : x_ext.IsAmalgamation (R := S.arrows) t)
    (t_uniq :
      ∀ (y : obj (obj yoneda W) (op X)),
        (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t),
    ∃! t : obj (obj yoneda W) (op X), x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t
⊢ ∃! t : obj (obj yoneda W) (op X), x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t

Tactic:
obtain ⟨t, t_amalg, t_uniq⟩ :=
    (Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext

Premises used: Iff.mpr, Nonempty.intro, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
⊢ ∃! t : obj (obj yoneda W) (op X), x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t

Tactic:
⟨t, ?_, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
refine_1 :
  (fun (t : obj (obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t) t
refine_2 :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t)
        y →
      y = t
⊢ ∃! t : obj (obj yoneda W) (op X), x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t

Tactic:
refine ⟨t, ?_, ?_⟩