-- Mathlib.CategoryTheory.Monoidal.Free.Basic
_private.Mathlib.CategoryTheory.Monoidal.Free.Basic.0.CategoryTheory.FreeMonoidalCategory.projectMapAux.match_1.eq_4 : ∀ {C : Type u_1} (motive : (x x_1 : CategoryTheory.FreeMonoidalCategory C) → x.Hom x_1 → Sort u_2)
  (a : CategoryTheory.FreeMonoidalCategory C)
  (h_1 : (x : CategoryTheory.FreeMonoidalCategory C) → motive x x (CategoryTheory.FreeMonoidalCategory.Hom.id x))
  (h_2 :
    (X Y Z : CategoryTheory.FreeMonoidalCategory C) →
      motive ((X.tensor Y).tensor Z) (X.tensor (Y.tensor Z)) (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z))
  (h_3 :
    (X Y Z : CategoryTheory.FreeMonoidalCategory C) →
      motive (X.tensor (Y.tensor Z)) ((X.tensor Y).tensor Z) (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z))
  (h_4 :
    (a : CategoryTheory.FreeMonoidalCategory C) →
      motive (CategoryTheory.FreeMonoidalCategory.unit.tensor a) a (CategoryTheory.FreeMonoidalCategory.Hom.l_hom a))
  (h_5 :
    (a : CategoryTheory.FreeMonoidalCategory C) →
      motive a (CategoryTheory.FreeMonoidalCategory.unit.tensor a) (CategoryTheory.FreeMonoidalCategory.Hom.l_inv a))
  (h_6 :
    (a : CategoryTheory.FreeMonoidalCategory C) →
      motive (a.tensor CategoryTheory.FreeMonoidalCategory.unit) a (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom a))
  (h_7 :
    (a : CategoryTheory.FreeMonoidalCategory C) →
      motive a (a.tensor CategoryTheory.FreeMonoidalCategory.unit) (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv a))
  (h_8 : (x x_1 Y : CategoryTheory.FreeMonoidalCategory C) → (f : x.Hom Y) → (g : Y.Hom x_1) → motive x x_1 (f.comp g))
  (h_9 :
    (X Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C) →
      (p : Y₁.Hom Y₂) → motive (X.tensor Y₁) (X.tensor Y₂) (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X p))
  (h_10 :
    (X₁ X₂ : CategoryTheory.FreeMonoidalCategory C) →
      (p : X₁.Hom X₂) →
        (X : CategoryTheory.FreeMonoidalCategory C) → motive (X₁.tensor X) (X₂.tensor X) (p.whiskerRight X))
  (h_11 :
    (W X Y Z : CategoryTheory.FreeMonoidalCategory C) →
      (f : W.Hom Y) → (g : X.Hom Z) → motive (W.tensor X) (Y.tensor Z) (f.tensor g)),
  (match CategoryTheory.FreeMonoidalCategory.unit.tensor a, a, CategoryTheory.FreeMonoidalCategory.Hom.l_hom a with
    | x, .(x), CategoryTheory.FreeMonoidalCategory.Hom.id .(x) => h_1 x
    | .((X.tensor Y).tensor Z), .(X.tensor (Y.tensor Z)), CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z =>
      h_2 X Y Z
    | .(X.tensor (Y.tensor Z)), .((X.tensor Y).tensor Z), CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z =>
      h_3 X Y Z
    | .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), a, CategoryTheory.FreeMonoidalCategory.Hom.l_hom .(a) =>
      h_4 a
    | a, .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), CategoryTheory.FreeMonoidalCategory.Hom.l_inv .(a) =>
      h_5 a
    | .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), a, CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom .(a) =>
      h_6 a
    | a, .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv .(a) =>
      h_7 a
    | x, x_1, f.comp g => h_8 x x_1 Y f g
    | .(X.tensor Y₁), .(X.tensor Y₂), CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X p => h_9 X Y₁ Y₂ p
    | .(X₁.tensor X), .(X₂.tensor X), p.whiskerRight X => h_10 X₁ X₂ p X
    | .(W.tensor X), .(Y.tensor Z), f.tensor g => h_11 W X Y Z f g) =
    h_4 a