-- Module: Mathlib.CategoryTheory.SmallObject.Construction
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst_3 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_4 :
  HasPushout (X := ∐ functorObjSrcFamily f πY) (Z := ∐ functorObjTgtFamily f πY)
    (functorObjTop f πY : ∐ functorObjSrcFamily f πY ⟶ Y)
    (functorObjLeft f πY : ∐ functorObjSrcFamily f πY ⟶ ∐ functorObjTgtFamily f πY)
h₀ :
  CategoryStruct.comp (Y :=
      pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
        (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (pushout.inl (functorObjTop f πX) (functorObjLeft f πX) :
        X ⟶
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (CategoryStruct.comp (Y := functorObj f πY) (functorMap f τ) (πFunctorObj f πY) : functorObj f πX ⟶ T) =
    CategoryStruct.comp (Y :=
      pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
        (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (pushout.inl (functorObjTop f πX) (functorObjLeft f πX) :
        X ⟶
          pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
            (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
            (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
      (πFunctorObj f πX ≫ Arrow.Hom.right τ : functorObj f πX ⟶ (Arrow.mk πY).right)
h₁ :
  ∀ (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b),
    Eq (α := functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶ T)
      (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjTgtFamily f πX)
        (CategoryStruct.comp (Y :=
            pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
              (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
              (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
            (pushout.inr (functorObjTop f πX) (functorObjLeft f πX) :
              ∐ functorObjTgtFamily f πX ⟶
                pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
                  (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
                  (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
            (CategoryStruct.comp (Y := functorObj f πY) (functorMap f τ) (πFunctorObj f πY) : functorObj f πX ⟶ T) :
          ∐ functorObjTgtFamily f πX ⟶ T))
      (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w } :
          functorObjTgtFamily f πX { i := i, t := t, b := b, w := w : FunctorObjIndex f πX } ⟶
            ∐ functorObjTgtFamily f πX)
        (CategoryStruct.comp (Y :=
            pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
              (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
              (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
            (pushout.inr (functorObjTop f πX) (functorObjLeft f πX) :
              ∐ functorObjTgtFamily f πX ⟶
                pushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
                  (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
                  (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX))
            (πFunctorObj f πX ≫ Arrow.Hom.right τ : functorObj f πX ⟶ (Arrow.mk πY).right) :
          ∐ functorObjTgtFamily f πX ⟶ T))
⊢ Eq (α := functorObj f πX ⟶ T) (CategoryStruct.comp (Y := functorObj f πY) (functorMap f τ) (πFunctorObj f πY))
    (πFunctorObj f πX ≫ Arrow.Hom.right τ)

Tactic:
ext ⟨i, t, b, w⟩