-- 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 : α
this :
  Eq (α := X a ⟶ W)
    (π a ≫
        H.desc
          { pt := W,
            ι :=
              {
                app := fun (x : (Sieve.generateFamily X π).arrows.category) ↦
                  ⋯.choose (p :=
                      fun
                        (g :
                          x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).left ⟶
                            X
                              (Exists.choose (p := fun (a : α) ↦
                                ∃ (g :
                                  x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).left ⟶
                                    X a),
                                  g ≫ π a =
                                    x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).hom)
                                ⋯)) ↦
                      g ≫
                          π
                            (Exists.choose (p := fun (a : α) ↦
                              ∃ (g :
                                x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).left ⟶
                                  X a),
                                g ≫ π a =
                                  x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).hom)
                              ⋯) =
                        x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).hom) ≫
                    e
                      (Exists.choose (p := fun (a : α) ↦
                        ∃ (g :
                          x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).left ⟶ X a),
                          g ≫ π a = x.obj (P := fun (f : Over.{v, u} B) ↦ (Sieve.generateFamily X π).arrows f.hom).hom)
                        ⋯),
                naturality := ⋯ :
                NatTrans (Sieve.generateFamily X π).arrows.diagram
                  (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) } } :
      X a ⟶ W)
    (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 ⟶ W)
⊢ π a ≫ H.desc (aux e ⋯) = e a
have rw : 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)) =
  e a
Tactic: rw [this]