-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorHom.match_1.eq_1 : ∀ (motive : (x₁ y₁ x₂ y₂ : AugmentedSimplexCategory) → (x₁ ⟶ y₁) → (x₂ ⟶ y₂) → Sort u_1)
  (a a_1 a_2 a_3 : SimplexCategory) (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (f₂ : CategoryTheory.WithInitial.of a_2 ⟶ CategoryTheory.WithInitial.of a_3)
  (h_1 :
    (a a_4 a_5 a_6 : SimplexCategory) →
      (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_4) →
        (f₂ : CategoryTheory.WithInitial.of a_5 ⟶ CategoryTheory.WithInitial.of a_6) →
          motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_4)
            (CategoryTheory.WithInitial.of a_5) (CategoryTheory.WithInitial.of a_6) 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_4 : SimplexCategory) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
        (f₂ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_4) →
          motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a)
            (CategoryTheory.WithInitial.of a_4) x f₂)
  (h_5 :
    (a a_4 : SimplexCategory) →
      (f₁ : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_4) →
        (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
          motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_4) 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.of a, CategoryTheory.WithInitial.of a_1, CategoryTheory.WithInitial.of a_2,
      CategoryTheory.WithInitial.of a_3, f₁, f₂ with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_4, CategoryTheory.WithInitial.of a_5,
      CategoryTheory.WithInitial.of a_6, f₁, f₂ => h_1 a a_4 a_5 a_6 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_4, x, f₂ => h_4 a a_4 x f₂
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_4, CategoryTheory.WithInitial.star,
      CategoryTheory.WithInitial.star, f₁, x => h_5 a a_4 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_1 a a_1 a_2 a_3 f₁ f₂