awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
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)) ⋯))
    (S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom) T h₃))
⊢ 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₃)

Tactic:
simp only [← hT, Category.assoc, H.fac _ h₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.EffectiveEpiFamilyStruct.fac
-- 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 : 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
⊢ 𝟙 (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_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 ⋯)
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)) ⋯) =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) T
        h₃)
⊢ 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₃))

Tactic:
change F.map i ≫ _ = _

Premises used: CategoryTheory.Functor.map
-- 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 : 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 ⋯)
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₃)
⊢ 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₃)

Tactic:
rw [S.w]

Premises used: CategoryTheory.Limits.Cocone.w
-- 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 : 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 ⋯)
⊢ 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:
rfl
-- 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 : 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
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)) ⋯))
      ⋯
⊢ 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)) ⋯))
      ⋯

Tactic:
dsimp
-- 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 : 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
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₁)) ⋯))
            (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₂
⊢ 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)) ⋯))
      ⋯

Tactic:
generalize_proofs h₁ 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 : 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₂)) ⋯))
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)) ⋯)
⊢ 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₂

Tactic:
apply H.uniq _ h₂

Premises used: CategoryTheory.EffectiveEpiFamilyStruct.uniq
-- 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 : 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₂)) ⋯))
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 : 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₂)) ⋯))
a : α
⊢ π a ≫ m =
    S.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom)
        (Over.mk (π a)) ⋯)

Tactic:
exact hm ⟨Over.mk (π a), a, 𝟙 _, by simp⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Over.mk, CategoryTheory.CategoryStruct.id, Exists.intro
-- 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
rw :
  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) ⋯))
⊢ 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

Tactic:
rw [Category.comp_id, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id
-- 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₁ :
  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) ⋯))
⊢ 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) ⋯))

Tactic:
apply h
-- 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₁ :
  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) ⋯))
⊢ 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) ⋯))

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc