-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorHom.match_1.eq_4 : ∀ (motive : (x₁ y₁ x₂ y₂ : AugmentedSimplexCategory) → (x₁ ⟶ y₁) → (x₂ ⟶ y₂) → Sort u_1) (a a_1 : SimplexCategory)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (f₂ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (h_1 :
    (a a_2 a_3 a_4 : SimplexCategory) →
      (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
        (f₂ : CategoryTheory.WithInitial.of a_3 ⟶ CategoryTheory.WithInitial.of a_4) →
          motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_2)
            (CategoryTheory.WithInitial.of a_3) (CategoryTheory.WithInitial.of a_4) f₁ f₂)
  (h_2 :
    (a y₁ y₂ : SimplexCategory) →
      (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of y₁) →
        (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of y₂) →
          motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of y₁) CategoryTheory.WithInitial.star
            (CategoryTheory.WithInitial.of y₂) f₁ x)
  (h_3 :
    (y₁ a y₂ : SimplexCategory) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of y₁) →
        (f₂ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of y₂) →
          motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of y₁) (CategoryTheory.WithInitial.of a)
            (CategoryTheory.WithInitial.of y₂) x f₂)
  (h_4 :
    (a a_2 : SimplexCategory) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
        (f₂ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
          motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a)
            (CategoryTheory.WithInitial.of a_2) x f₂)
  (h_5 :
    (a a_2 : SimplexCategory) →
      (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_2) →
        (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
          motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_2) CategoryTheory.WithInitial.star
            CategoryTheory.WithInitial.star f₁ x)
  (h_6 :
    (x x_1 : AugmentedSimplexCategory) →
      (x_2 : CategoryTheory.WithInitial.star ⟶ x) →
        (x_3 : CategoryTheory.WithInitial.star ⟶ x_1) →
          motive CategoryTheory.WithInitial.star x CategoryTheory.WithInitial.star x_1 x_2 x_3),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a,
      CategoryTheory.WithInitial.of a_1, x, f₂ with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_2, CategoryTheory.WithInitial.of a_3,
      CategoryTheory.WithInitial.of a_4, f₁, f₂ => h_1 a a_2 a_3 a_4 f₁ f₂
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of y₁, CategoryTheory.WithInitial.star,
      CategoryTheory.WithInitial.of y₂, f₁, x => h_2 a y₁ y₂ f₁ x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of y₁, CategoryTheory.WithInitial.of a,
      CategoryTheory.WithInitial.of y₂, x, f₂ => h_3 y₁ a y₂ x f₂
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a,
      CategoryTheory.WithInitial.of a_2, x, f₂ => h_4 a a_2 x f₂
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_2, CategoryTheory.WithInitial.star,
      CategoryTheory.WithInitial.star, f₁, x => h_5 a a_2 f₁ x
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.star, x_1, x_2, x_3 => h_6 x x_1 x_2 x_3) =
    h_4 a a_1 x f₂