awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B_1 : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B_1
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over.{v, u} B_1
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over.{v, u} B_1
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
a₁ :
  ∀ (h1 : ∃ (a : α) (g : B.left ⟶ X a), g ≫ π a = B.hom)
    (h2 :
      ∃ (g : B.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom))),
        g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom)) = B.hom)
    (h3 : ∃ (a : α) (g : A.left ⟶ X a), g ≫ π a = A.hom)
    (h4 :
      ∃ (g : A.left ⟶ X (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))),
        g ≫ π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom)) = A.hom),
    Over.Hom.left q ≫
        h2.choose (p := fun (g : B.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom))) ↦
            g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom)) = B.hom) ≫
          π (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom)) =
      h4.choose (p := fun (g : A.left ⟶ X (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))) ↦
          g ≫ π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom)) = A.hom) ≫
        π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))
⊢ Over.Hom.left q ≫
      CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) ⋯))
        (Exists.choose (p :=
          fun (g : B.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) ⋯)) ↦
          g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) ⋯) = B.hom) ⋯)
        (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) ⋯)) =
    CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) ⋯))
      (Exists.choose (p :=
        fun (g : A.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) ⋯)) ↦
        g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) ⋯) = A.hom) ⋯)
      (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) ⋯))

Tactic:
generalize_proofs h1 h2 h3 h4
-- Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
Goal:
C : Type u
inst : Category.{v, u} C
B_1 : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B_1
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
A : Over.{v, u} B_1
a : α
g₁ : A.left ⟶ X a
ha : g₁ ≫ π a = A.hom
B : Over.{v, u} B_1
b : α
g₂ : B.left ⟶ X b
hb : g₂ ≫ π b = B.hom
q : A ⟶ B
h1 : ∃ (a : α) (g : B.left ⟶ X a), g ≫ π a = B.hom
h2 :
  ∃ (g : B.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom))),
    g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom)) = B.hom
h3 : ∃ (a : α) (g : A.left ⟶ X a), g ≫ π a = A.hom
h4 :
  ∃ (g : A.left ⟶ X (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))),
    g ≫ π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom)) = A.hom
a₁ :
  Over.Hom.left q ≫ B.hom =
    h4.choose (p := fun (g : A.left ⟶ X (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))) ↦
        g ≫ π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom)) = A.hom) ≫
      π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))
a₂ : Over.Hom.left q ≫ B.hom = A.hom
a₃ a₄ : A.hom = A.hom
⊢ Over.Hom.left q ≫
      h2.choose (p := fun (g : B.left ⟶ X (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom))) ↦
          g ≫ π (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom)) = B.hom) ≫
        π (h1.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom)) =
    h4.choose (p := fun (g : A.left ⟶ X (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))) ↦
        g ≫ π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom)) = A.hom) ≫
      π (h3.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom))

Tactic:
rw [h2.choose_spec, h4.choose_spec, Over.w]

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

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

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

Tactic:
rw [← Category.id_comp (e a)]

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

Tactic:
conv_rhs => rw [← Category.id_comp (e a)]

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

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

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

Tactic:
rw [h2.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
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
aux : {W : C} →
  (e : (a : α) → X a ⟶ W) →
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) →
      Cocone (Sieve.generateFamily X π).arrows.diagram :=
  fun {W : C} (e : (a : α) → X a ⟶ W)
      (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂) ↦
    { pt := W,
      ι :=
        {
          app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
            match (motive :=
              (x : (Sieve.generateFamily X π).arrows.category) →
                (Sieve.generateFamily X π).arrows.diagram.obj x ⟶
                  Functor.obj (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) x)
              x with
            | { obj := obj, property := hT } =>
              ⋯.choose (p :=
                  fun
                    (g :
                      obj.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT)) ↦
                  g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT) = obj.hom) ≫
                e (Exists.choose (p := fun (a : α) ↦ ∃ (g : obj.left ⟶ X a), g ≫ π a = obj.hom) hT),
          naturality := ⋯ :
          NatTrans (Sieve.generateFamily X π).arrows.diagram
            (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } }
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
x :
  ∀ (j : (Sieve.generateFamily X π).arrows.category),
    (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = (aux e ⋯).ι.app j
⊢ m = H.desc (aux e ⋯)

Tactic:
apply H.uniq (aux e h)

Premises used: CategoryTheory.Limits.IsColimit.uniq