awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) ⋯))
      (Over.Hom.left q ≫
        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) ⋯))
have a₁ : Over.Hom.left q ≫
    CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry))
      (Exists.choose (p :=
        fun (g : B.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry)) ↦
        g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry) = B.hom) sorry)
      (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry)) =
  CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) sorry))
    (Exists.choose (p :=
      fun (g : A.left ⟶ X (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) sorry)) ↦
      g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) sorry) = A.hom) sorry)
    (π (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) sorry))
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ 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) ⋯))
have 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))
Tactic: generalize_proofs h1 h2 h3 h4
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ 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))
have 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))
Tactic: rw [h2.choose_spec, h4.choose_spec, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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))
⊢ 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))
have a₂ : Over.Hom.left q ≫ B.hom = A.hom
Tactic: rw [h2.choose_spec, h4.choose_spec, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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
⊢ 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))
have a₃ : A.hom = A.hom
Tactic: rw [h2.choose_spec, h4.choose_spec, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (hypothesis)
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 ≫ H.desc (aux e ⋯) = e a
have this : 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)) sorry) ⟶
    (aux e sorry).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)) sorry) ≫
    H.desc (aux e sorry))
  ((aux e sorry).ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
      (Over.mk (π a)) sorry))
Tactic: have := H.fac (aux e h) ⟨Over.mk (π a), a, 𝟙 _, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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 : α
| e a
have rw : 𝟙 (X a) ≫ e a
Tactic: rw [← Category.id_comp (e a)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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 : α
⊢ 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
have conv_rhs : CategoryStruct.comp (Y := X (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry))
    (Exists.choose (p :=
      fun (g : X a ⟶ X (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry)) ↦
      g ≫ π (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry) = π a) sorry)
    (e (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry)) =
  𝟙 (X a) ≫ e a
Tactic: conv_rhs => rw [← Category.id_comp (e a)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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 : α
⊢ 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
have a₁ : CategoryStruct.comp (Y := X (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry))
    (Exists.choose (p :=
      fun (g : X a ⟶ X (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry)) ↦
      g ≫ π (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry) = π a) sorry)
    (π (Exists.choose (p := fun (a_1 : α) ↦ ∃ (g : X a ⟶ X a_1), g ≫ π a_1 = π a) sorry)) =
  𝟙 (X a) ≫ π a
Tactic: apply h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EffectiveEpimorphic (goal)
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 : α
⊢ 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
have 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
Tactic: generalize_proofs h1 h2