-- 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
⊢ Eq (α :=
    (Sieve.generateFamily X π).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) A
          ⋯) ⟶
      Functor.obj (C := (Sieve.generateFamily X π).arrows.category)
        (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) B
          ⋯))
    (CategoryStruct.comp (Y :=
      (Sieve.generateFamily X π).arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) B
          ⋯))
      ((Sieve.generateFamily X π).arrows.diagram.map { hom := q })
      (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)
        ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) B
          ⋯ 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)))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := (Sieve.generateFamily X π).arrows.category)
        (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) A
          ⋯))
      (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)
        ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} B_1) ↦ (Sieve.generateFamily X π).arrows f.hom) A
          ⋯ 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))
      (Functor.map (Functor.obj (Functor.const (Sieve.generateFamily X π).arrows.category) W) { hom := q }))
have dsimp : 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)
      (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)) ≫
    𝟙 W
Tactic: dsimp