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 : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
h : g₁ ≫ π a₁ = g₂ ≫ π a₂
A₁ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₁)) ⋯
A₂ : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a₂)) ⋯
Z' : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (g₁ ≫ π a₁)) ⋯
i₁ : Z' ⟶ A₁ :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g₁ ⋯)
i₂ : Z' ⟶ A₂ :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g₂ ⋯)
⊢ Eq (α := Z ⟶ S.pt)
    (g₁ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₁)) ⋯))
    (g₂ ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a₂)) ⋯))
have change : F.map i₁ ≫
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
        (Over.mk (π a₁)) sorry) =
  F.map i₂ ≫
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
        (Over.mk (π a₂)) sorry)
Tactic: change F.map i₁ ≫ _ = F.map i₂ ≫ _
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
⊢ ∀ (j : (Sieve.generateFamily X π).arrows.category),
    (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫
        H.desc
          (fun (a : α) ↦
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a)) ⋯))
          ⋯ =
      S.ι.app j
have X₁ : ∀ (T : Over.{v, u} B) (a : α) (g : T.left ⟶ X a) (hT : g ≫ π a = T.hom),
  Eq (α :=
    (Sieve.generateFamily X π).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          sorry) ⟶
      S.pt)
    ((Sieve.generateFamily X π).arrows.cocone.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          sorry) ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) sorry))
        sorry)
    (S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T sorry))
Tactic: ⟨T, a, (g : T.left ⟶ X a), hT⟩
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
⊢ Eq (α :=
    (Sieve.generateFamily X π).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          ⋯) ⟶
      S.pt)
    ((Sieve.generateFamily X π).arrows.cocone.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T
          ⋯) ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) ⋯))
        ⋯)
    (S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯))
have dsimp : T.hom ≫
    H.desc
      (fun (a : α) ↦
        S.ι.app
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
            (Over.mk (π a)) sorry))
      sorry =
  S.ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T sorry)
Tactic: dsimp
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
⊢ T.hom ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) ⋯))
        ⋯ =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T ⋯)
have generalize_proofs : ∀ (h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom)
  (h₂ :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      g₁ ≫ π a₁ = g₂ ≫ π a₂ →
        Eq (α := Z ⟶ S.pt)
          (g₁ ≫
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₁)) sorry))
          (g₂ ≫
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₂)) sorry)))
  (h₃ : (Sieve.generateFamily X π).arrows T.hom),
  T.hom ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) sorry))
        @h₂ =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T h₃)
Tactic: generalize_proofs h₁ h₂ 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      Eq (α := Z ⟶ S.pt)
        (g₁ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a₁)) ⋯))
        (g₂ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a₂)) ⋯))
h₃ : (Sieve.generateFamily X π).arrows T.hom
⊢ T.hom ≫
      H.desc
        (fun (a : α) ↦
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a)) ⋯))
        @h₂ =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T h₃)
have simp : Eq (α := T.left ⟶ S.pt)
  (g ≫
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
        (Over.mk (π a)) sorry))
  (S.ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T h₃))
Tactic: simp only [← hT, Category.assoc, H.fac _ h₂]
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B_1) fun (T : Over.{v, u} B_1) ↦
    (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B_1
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      Eq (α := Z ⟶ S.pt)
        (g₁ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦
              (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₁)) ⋯))
        (g₂ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦
              (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₂)) ⋯))
h₃ : (Sieve.generateFamily X π).arrows T.hom
A : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a)) ⋯
B : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk T.hom) ⋯
i : B ⟶ A :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g ⋯)
⊢ Eq (α := T.left ⟶ S.pt)
    (g ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a)) ⋯))
    (S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) T
        h₃))
have change : F.map i ≫
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom)
        (Over.mk (π a)) sorry) =
  S.ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) T h₃)
Tactic: change F.map i ≫ _ = _
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B_1) fun (T : Over.{v, u} B_1) ↦
    (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
T : Over.{v, u} B_1
a : α
g : T.left ⟶ X a
hT : g ≫ π a = T.hom
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      Eq (α := Z ⟶ S.pt)
        (g₁ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦
              (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₁)) ⋯))
        (g₂ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦
              (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₂)) ⋯))
h₃ : (Sieve.generateFamily X π).arrows T.hom
A : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk (π a)) ⋯
B : D :=
  ObjectProperty.FullSubcategory.mk (P := fun (T : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows T.hom)
    (Over.mk T.hom) ⋯
i : B ⟶ A :=
  ObjectProperty.homMk (P := fun (T : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows T.hom) (Over.homMk g ⋯)
⊢ F.map i ≫
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a)) ⋯) =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) T
        h₃)
have rw : S.ι.app B =
  S.ι.app
    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) T h₃)
Tactic: rw [S.w]
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
⊢ m =
    H.desc
      (fun (a : α) ↦
        S.ι.app
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
            (Over.mk (π a)) ⋯))
      ⋯
have dsimp : m =
  H.desc
    (fun (a : α) ↦
      S.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
          (Over.mk (π a)) sorry))
    sorry
Tactic: dsimp
-- 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
⊢ m =
    H.desc
      (fun (a : α) ↦
        S.ι.app
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
            (Over.mk (π a)) ⋯))
      ⋯
have generalize_proofs : ∀ (h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom)
  (h₂ :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      g₁ ≫ π a₁ = g₂ ≫ π a₂ →
        Eq (α := Z ⟶ S.pt)
          (g₁ ≫
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₁)) sorry))
          (g₂ ≫
            S.ι.app
              (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦
                (Sieve.generateFamily X π).arrows f.hom) (Over.mk (π a₂)) sorry))),
  m =
    H.desc
      (fun (a : α) ↦
        S.ι.app
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
            (Over.mk (π a)) sorry))
      @h₂
Tactic: generalize_proofs h₁ 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 : EffectiveEpiFamilyStruct X π
D : Type (max u v) :=
  ObjectProperty.FullSubcategory (C := Over.{v, u} B) fun (T : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows T.hom
F : D ⥤ C := (Sieve.generateFamily X π).arrows.diagram
S : Cocone (Sieve.generateFamily X π).arrows.diagram
m : (Sieve.generateFamily X π).arrows.cocone.pt ⟶ S.pt
hm :
  ∀ (j : (Sieve.generateFamily X π).arrows.category), (Sieve.generateFamily X π).arrows.cocone.ι.app j ≫ m = S.ι.app j
h₁ : ∀ (a : α), (Sieve.generateFamily X π).arrows (Over.mk (π a)).hom
h₂ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ →
      Eq (α := Z ⟶ S.pt)
        (g₁ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a₁)) ⋯))
        (g₂ ≫
          S.ι.app
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
              (Over.mk (π a₂)) ⋯))
⊢ m =
    H.desc
      (fun (a : α) ↦
        S.ι.app
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
            (Over.mk (π a)) ⋯))
      @h₂
have a : ∀ (a : α),
  π a ≫ m =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
        (Over.mk (π a)) sorry)
Tactic: apply H.uniq _ h₂
-- 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) ⋯)
        (e (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) ⋯)
        (e (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) ⋯)) ≫
      𝟙 W
have rw : CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry))
    (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) sorry)) ↦
        g ≫ π (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry) = B.hom) sorry)
    (e (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)
    (e (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) sorry))
Tactic: rw [Category.comp_id, ← 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
⊢ 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) ⋯)
      (e (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) ⋯)
      (e (Exists.choose (p := fun (a : α) ↦ ∃ (g : A.left ⟶ X a), g ≫ π a = A.hom) ⋯))
have a₁ : CategoryStruct.comp (Y := X (Exists.choose (p := fun (a : α) ↦ ∃ (g : B.left ⟶ X a), g ≫ π a = B.hom) sorry))
    (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) 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: apply h