∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} [inst_1 : SizeOf C] [inst_2 : SizeOf α] (ι : Type w) (π : ι → α)
  (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)) (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i))
  (isColimit₁ : CategoryTheory.Limits.IsColimit cofan₁) (isColimit₂ : CategoryTheory.Limits.IsColimit cofan₂)
  (m : cofan₁.pt ⟶ cofan₂.pt)
  (hm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
          CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam)
  (g₁ : cofan₁.pt ⟶ X₁) (g₂ : cofan₂.pt ⟶ X₂) (isPushout : CategoryTheory.IsPushout g₁ m f g₂),
  sizeOf
      { ι := ι, π := π, cofan₁ := cofan₁, cofan₂ := cofan₂, isColimit₁ := isColimit₁, isColimit₂ := isColimit₂, m := m,
        hm := hm, g₁ := g₁, g₂ := g₂, isPushout := isPushout } =
    1 + sizeOf ι + sizeOf cofan₁ + sizeOf cofan₂ + sizeOf isColimit₁ + sizeOf isColimit₂ + sizeOf m + sizeOf g₁ +
        sizeOf g₂ +
      sizeOf isPushout