∀ {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₂} (ι : 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₂) (ι_1 : Type w)
  (π_1 : ι_1 → α) (cofan₁_1 : CategoryTheory.Limits.Cofan fun i => A (π_1 i))
  (cofan₂_1 : CategoryTheory.Limits.Cofan fun i => B (π_1 i)) (isColimit₁_1 : CategoryTheory.Limits.IsColimit cofan₁_1)
  (isColimit₂_1 : CategoryTheory.Limits.IsColimit cofan₂_1) (m_1 : cofan₁_1.pt ⟶ cofan₂_1.pt)
  (hm_1 :
    autoParam
      (∀ (i : ι_1),
        CategoryTheory.CategoryStruct.comp (cofan₁_1.inj i) m_1 =
          CategoryTheory.CategoryStruct.comp (g (π_1 i)) (cofan₂_1.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam)
  (g₁_1 : cofan₁_1.pt ⟶ X₁) (g₂_1 : cofan₂_1.pt ⟶ X₂) (isPushout_1 : CategoryTheory.IsPushout g₁_1 m_1 f g₂_1),
  ({ ι := ι, π := π, cofan₁ := cofan₁, cofan₂ := cofan₂, isColimit₁ := isColimit₁, isColimit₂ := isColimit₂, m := m,
        hm := hm, g₁ := g₁, g₂ := g₂, isPushout := isPushout } =
      { ι := ι_1, π := π_1, cofan₁ := cofan₁_1, cofan₂ := cofan₂_1, isColimit₁ := isColimit₁_1,
        isColimit₂ := isColimit₂_1, m := m_1, hm := hm_1, g₁ := g₁_1, g₂ := g₂_1, isPushout := isPushout_1 }) =
    (ι = ι_1 ∧
      π ≍ π_1 ∧
        cofan₁ ≍ cofan₁_1 ∧
          cofan₂ ≍ cofan₂_1 ∧ isColimit₁ ≍ isColimit₁_1 ∧ isColimit₂ ≍ isColimit₂_1 ∧ m ≍ m_1 ∧ g₁ ≍ g₁_1 ∧ g₂ ≍ g₂_1)