awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
simp_rw : R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) (Sieve.generate R).arrows
simp_rw₁ :
  (Sieve.generate R).EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) (Sieve.generate R).arrows
⊢ R.EffectiveEpimorphic ↔ ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R

Tactic:
simp_rw [Presieve.isSheafFor_iff_generate R,
    Presieve.EffectiveEpimorphic, Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda]

Premises used: CategoryTheory.Sieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda, CategoryTheory.Presieve.isSheafFor_iff_generate, CategoryTheory.Presieve.EffectiveEpimorphic
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : R.EffectiveEpimorphic
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
rw :
  ∀ (hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R) (F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w))
    [F.IsRepresentable], IsSheafFor F R
⊢ IsSheafFor F R

Tactic:
rw [Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda] at hR

Premises used: CategoryTheory.Presieve.EffectiveEpimorphic.iff_forall_isSheafFor_yoneda
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
rw : IsSheafFor (F ⋙ uliftFunctor.{v, w}) R
⊢ IsSheafFor F R

Tactic:
rw [← isSheafFor_comp_uliftFunctor_iff]

Premises used: CategoryTheory.Presieve.isSheafFor_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor (F ⋙ uliftFunctor.{v, w}) R

Tactic:
Presieve.isSheafFor_iso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_

Premises used: CategoryTheory.Functor.uliftYonedaReprXIso, CategoryTheory.Functor.comp, CategoryTheory.Presieve.isSheafFor_iso, CategoryTheory.uliftFunctor
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
refine : IsSheafFor (Functor.obj uliftYoneda.{w, v, u} (F ⋙ uliftFunctor.{v, w}).reprX) R
⊢ IsSheafFor (F ⋙ uliftFunctor.{v, w}) R

Tactic:
refine Presieve.isSheafFor_iso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
rw : IsSheafFor (Functor.obj yoneda (F ⋙ uliftFunctor.{v, w}).reprX) R
⊢ IsSheafFor (Functor.obj yoneda (F ⋙ uliftFunctor.{v, w}).reprX ⋙ uliftFunctor.{w, v}) R

Tactic:
rw [isSheafFor_comp_uliftFunctor_iff]

Premises used: CategoryTheory.Presieve.isSheafFor_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor (Functor.obj yoneda (F ⋙ uliftFunctor.{v, w}).reprX) R

Tactic:
hR _
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
R : Presieve.{v, u} X
hR : ∀ (Y : C), IsSheafFor (Functor.obj yoneda Y) R
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
inst_1 : F.IsRepresentable
⊢ IsSheafFor (Functor.obj yoneda (F ⋙ uliftFunctor.{v, w}).reprX) R

Tactic:
exact hR _
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
dsimp :
  Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ e =
    (Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e) ≫ 𝟙 W
⊢ Eq (α :=
    (Sieve.generateSingleton f).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A hA) ⟶
      Functor.obj (C := (Sieve.generateSingleton f).arrows.category)
        (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W)
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          B hB))
    (CategoryStruct.comp (Y :=
      (Sieve.generateSingleton f).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          B hB))
      ((Sieve.generateSingleton f).arrows.diagram.map { hom := q })
      (match (motive :=
        (x : (Sieve.generateSingleton f).arrows.category) →
          (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
            Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
        ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          B hB with
      | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := (Sieve.generateSingleton f).arrows.category)
        (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W)
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A hA))
      (match (motive :=
        (x : (Sieve.generateSingleton f).arrows.category) →
          (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
            Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
        ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A hA with
      | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e)
      (Functor.map (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) { hom := q }))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
simp :
  (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ e =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e
⊢ Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ e =
    (Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e) ≫ 𝟙 W

Tactic:
simp only [← Category.assoc, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
a :
  (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
⊢ (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ e =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ e

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
A : Over.{v, u} X
hA : (Sieve.generateSingleton f).arrows A.hom
B : Over.{v, u} X
hB : (Sieve.generateSingleton f).arrows B.hom
q : A ⟶ B
a :
  Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
a₁ : Over.Hom.left q ≫ B.hom = Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f
a₂ : Over.Hom.left q ≫ B.hom = A.hom
a₃ a₄ : A.hom = A.hom
⊢ (Over.Hom.left q ≫ Exists.choose (p := fun (e : B.left ⟶ Y) ↦ e ≫ f = B.hom) hB) ≫ f =
    Exists.choose (p := fun (e : A.left ⟶ Y) ↦ e ≫ f = A.hom) hA ≫ f

Tactic:
rw [Category.assoc, hB.choose_spec, hA.choose_spec, Over.w]

Premises used: CategoryTheory.Category.assoc, Exists.choose_spec, CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ 𝟙 (Over.mk f).left ≫ f = (Over.mk f).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
⊢ Eq (α :=
    (Sieve.generateSingleton f).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          (Over.mk f) ⋯) ⟶
      (aux e ⋯).pt)
    ((Sieve.generateSingleton f).arrows.cocone.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          (Over.mk f) ⋯) ≫
      Hf.desc (aux e ⋯))
    ((aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
        (Over.mk f) ⋯))

Tactic:
have := Hf.fac (aux e h) ⟨Over.mk f, 𝟙 _, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
this :
  Eq (α := Y ⟶ W)
    (f ≫
        Hf.desc
          { pt := W,
            ι :=
              {
                app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
                  Exists.choose (p :=
                      fun
                        (e :
                          x.obj (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom).left ⟶
                            Y) ↦
                      e ≫ f = x.obj (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom).hom)
                      ⋯ ≫
                    e,
                naturality := ⋯ :
                NatTrans (Sieve.generateSingleton f).arrows.diagram
                  (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } } :
      Y ⟶ W)
    (Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ e : Y ⟶ W)
rw : Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ e = e
⊢ f ≫ Hf.desc (aux e ⋯) = e

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
nth_rewrite : Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ e = 𝟙 Y ≫ e
⊢ Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ e = e

Tactic:
nth_rewrite 2 [← Category.id_comp e]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
a : Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ f = 𝟙 Y ≫ f
⊢ Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ e = 𝟙 Y ≫ e

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
a : ∀ (hh : ∃ (e : Y ⟶ Y), e ≫ f = f), hh.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ≫ f = 𝟙 Y ≫ f
⊢ Exists.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ⋯ ≫ f = 𝟙 Y ≫ f

Tactic:
generalize_proofs hh
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
hh : ∃ (e : Y ⟶ Y), e ≫ f = f
a : f = 𝟙 Y ≫ f
a₁ a₂ : f = f
⊢ hh.choose (p := fun (e : Y ⟶ Y) ↦ e ≫ f = f) ≫ f = 𝟙 Y ≫ f

Tactic:
rw [hh.choose_spec, Category.id_comp]

Premises used: Exists.choose_spec, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
x :
  ∀ (j : (Sieve.generateSingleton f).arrows.category),
    (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ m = (aux e ⋯).ι.app j
⊢ m = Hf.desc (aux e ⋯)

Tactic:
apply Hf.uniq (aux e h)

Premises used: CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : IsColimit (Sieve.generateSingleton f).arrows.cocone
aux : {W : C} →
  (e : Y ⟶ W) →
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) →
      Cocone (Sieve.generateSingleton f).arrows.diagram :=
  fun {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateSingleton f).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateSingleton f).arrows.category) →
                (Sieve.generateSingleton f).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } => Exists.choose (p := fun (e : obj.left ⟶ Y) ↦ e ≫ f = obj.hom) hT ≫ e,
          naturality := ⋯ :
          NatTrans (Sieve.generateSingleton f).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateSingleton f).arrows.category) W) } }
W : C
e : Y ⟶ W
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e
m : X ⟶ W
hm : f ≫ m = e
A : Over.{v, u} X
g : A.left ⟶ Y
hA : g ≫ f = A.hom
x :
  A.hom ≫ m =
    (aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom) A
        ⋯)
⊢ Eq (α :=
    (Sieve.generateSingleton f).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A ⋯) ⟶
      (aux e ⋯).pt)
    ((Sieve.generateSingleton f).arrows.cocone.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom)
          A ⋯) ≫
      m)
    ((aux e ⋯).ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f_1 : Over.{v, u} X) ↦ (Sieve.generateSingleton f).arrows f_1.hom) A
        ⋯))

Tactic:
dsimp