-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
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)
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))
      (functorMap f (𝟙 (Arrow.mk πX)) : functorObj f πX ⟶ functorObj 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.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) : functorObj f πX ⟶ functorObj f πX)
⊢ functorMap f (𝟙 (Arrow.mk πX)) = 𝟙 (functorObj f πX)
have 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 } ⟶ functorObj f πX)
    (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))
          (functorMap f (𝟙 (Arrow.mk πX)) : functorObj f πX ⟶ functorObj f πX) :
        ∐ functorObjTgtFamily f πX ⟶ functorObj f πX))
    (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) : functorObj f πX ⟶ functorObj f πX) :
        ∐ functorObjTgtFamily f πX ⟶ functorObj f πX))
Tactic: ext ⟨i, t, b, w⟩