-- 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 X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  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_3 : HasPushouts.{v, u} C
inst_4 : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow.{v, u} C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
h₁ :
  Eq (α :=
    π₁.left ⟶
      pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
        (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
        (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
    (CategoryStruct.comp (Y :=
        pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
          (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
          (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
        (pushout.inl (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) :
          π₁.left ⟶
            pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
              (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
              (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
        (pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom)
            (functorObjLeft f π₃.hom) (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ'))
            (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ :
          pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
              (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
              (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom) ⟶
            pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
              (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
              (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
      π₁.left ⟶
        pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
          (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
          (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
    (CategoryStruct.comp (Y :=
        pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
          (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
          (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
        (pushout.inl (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) :
          π₁.left ⟶
            pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
              (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
              (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
        (CategoryStruct.comp (Y := functorObj f π₂.hom)
            (pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom)
                (functorObjLeft f π₂.hom) (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ :
              pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                  (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                  (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom) ⟶
                pushout (X := ∐ functorObjSrcFamily f π₂.hom) (Z := ∐ functorObjTgtFamily f π₂.hom)
                  (functorObjTop f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ π₂.left)
                  (functorObjLeft f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ ∐ functorObjTgtFamily f π₂.hom))
            (pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom)
                (functorObjLeft f π₃.hom) (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯ :
              pushout (X := ∐ functorObjSrcFamily f π₂.hom) (Z := ∐ functorObjTgtFamily f π₂.hom)
                  (functorObjTop f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ π₂.left)
                  (functorObjLeft f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ ∐ functorObjTgtFamily f π₂.hom) ⟶
                pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
                  (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
                  (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
          functorObj f π₁.hom ⟶ functorObj f π₃.hom) :
      π₁.left ⟶
        pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
          (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
          (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
h₂ :
  ∀ (i : I) (t : A i ⟶ π₁.left) (b : B i ⟶ π₁.right) (w : t ≫ π₁.hom = f i ≫ b),
    Eq (α :=
      functorObjTgtFamily f π₁.hom { i := i, t := t, b := b, w := w : FunctorObjIndex f π₁.hom } ⟶
        pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
          (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
          (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
      (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f π₁.hom)
          (Sigma.ι (functorObjTgtFamily f π₁.hom) { i := i, t := t, b := b, w := w } :
            functorObjTgtFamily f π₁.hom { i := i, t := t, b := b, w := w : FunctorObjIndex f π₁.hom } ⟶
              ∐ functorObjTgtFamily f π₁.hom)
          (CategoryStruct.comp (Y :=
              pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
              (pushout.inr (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) :
                ∐ functorObjTgtFamily f π₁.hom ⟶
                  pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                    (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                    (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
              (pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom)
                  (functorObjLeft f π₃.hom) (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ'))
                  (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ :
                pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                    (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                    (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom) ⟶
                  pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
                    (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
                    (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
            ∐ functorObjTgtFamily f π₁.hom ⟶
              pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
                (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
                (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
        functorObjTgtFamily f π₁.hom { i := i, t := t, b := b, w := w : FunctorObjIndex f π₁.hom } ⟶
          pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
            (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
            (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
      (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f π₁.hom)
          (Sigma.ι (functorObjTgtFamily f π₁.hom) { i := i, t := t, b := b, w := w } :
            functorObjTgtFamily f π₁.hom { i := i, t := t, b := b, w := w : FunctorObjIndex f π₁.hom } ⟶
              ∐ functorObjTgtFamily f π₁.hom)
          (CategoryStruct.comp (Y :=
              pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
              (pushout.inr (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) :
                ∐ functorObjTgtFamily f π₁.hom ⟶
                  pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                    (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                    (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom))
              (CategoryStruct.comp (Y := functorObj f π₂.hom)
                  (pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom)
                      (functorObjLeft f π₂.hom) (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ :
                    pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
                        (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
                        (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom) ⟶
                      pushout (X := ∐ functorObjSrcFamily f π₂.hom) (Z := ∐ functorObjTgtFamily f π₂.hom)
                        (functorObjTop f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ π₂.left)
                        (functorObjLeft f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ ∐ functorObjTgtFamily f π₂.hom))
                  (pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom)
                      (functorObjLeft f π₃.hom) (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯ :
                    pushout (X := ∐ functorObjSrcFamily f π₂.hom) (Z := ∐ functorObjTgtFamily f π₂.hom)
                        (functorObjTop f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ π₂.left)
                        (functorObjLeft f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ ∐ functorObjTgtFamily f π₂.hom) ⟶
                      pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
                        (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
                        (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
                functorObj f π₁.hom ⟶ functorObj f π₃.hom) :
            ∐ functorObjTgtFamily f π₁.hom ⟶
              pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
                (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
                (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
        functorObjTgtFamily f π₁.hom { i := i, t := t, b := b, w := w : FunctorObjIndex f π₁.hom } ⟶
          pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
            (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
            (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
⊢ Eq (α := functorObj f π₁.hom ⟶ functorObj f π₃.hom)
    (pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₃.hom) (functorObjLeft f π₃.hom)
        (Arrow.Hom.left τ ≫ Arrow.Hom.left τ') (functorMapTgt f (τ ≫ τ')) (functorMapSrc f (τ ≫ τ')) ⋯ ⋯ :
      pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
          (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
          (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom) ⟶
        pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
          (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
          (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom))
    (CategoryStruct.comp (Y := functorObj f π₂.hom)
        (pushout.map (functorObjTop f π₁.hom) (functorObjLeft f π₁.hom) (functorObjTop f π₂.hom)
            (functorObjLeft f π₂.hom) (Arrow.Hom.left τ) (functorMapTgt f τ) (functorMapSrc f τ) ⋯ ⋯ :
          pushout (X := ∐ functorObjSrcFamily f π₁.hom) (Z := ∐ functorObjTgtFamily f π₁.hom)
              (functorObjTop f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ π₁.left)
              (functorObjLeft f π₁.hom : ∐ functorObjSrcFamily f π₁.hom ⟶ ∐ functorObjTgtFamily f π₁.hom) ⟶
            pushout (X := ∐ functorObjSrcFamily f π₂.hom) (Z := ∐ functorObjTgtFamily f π₂.hom)
              (functorObjTop f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ π₂.left)
              (functorObjLeft f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ ∐ functorObjTgtFamily f π₂.hom))
        (pushout.map (functorObjTop f π₂.hom) (functorObjLeft f π₂.hom) (functorObjTop f π₃.hom)
            (functorObjLeft f π₃.hom) (Arrow.Hom.left τ') (functorMapTgt f τ') (functorMapSrc f τ') ⋯ ⋯ :
          pushout (X := ∐ functorObjSrcFamily f π₂.hom) (Z := ∐ functorObjTgtFamily f π₂.hom)
              (functorObjTop f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ π₂.left)
              (functorObjLeft f π₂.hom : ∐ functorObjSrcFamily f π₂.hom ⟶ ∐ functorObjTgtFamily f π₂.hom) ⟶
            pushout (X := ∐ functorObjSrcFamily f π₃.hom) (Z := ∐ functorObjTgtFamily f π₃.hom)
              (functorObjTop f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ π₃.left)
              (functorObjLeft f π₃.hom : ∐ functorObjSrcFamily f π₃.hom ⟶ ∐ functorObjTgtFamily f π₃.hom)) :
      functorObj f π₁.hom ⟶ functorObj f π₃.hom)

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