-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeMapAux.match_3.eq_5 : ∀ {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 :
    (T X Y W : CategoryTheory.FreeMonoidalCategory C) →
      (f : T.Hom Y) → (g : X.Hom W) → motive (T.tensor X) (Y.tensor W) (f.tensor g))
  (h_10 :
    (T Y₁ W : CategoryTheory.FreeMonoidalCategory C) →
      (f : Y₁.Hom W) → motive (T.tensor Y₁) (T.tensor W) (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft T f))
  (h_11 :
    (T X₂ : CategoryTheory.FreeMonoidalCategory C) →
      (f : T.Hom X₂) →
        (W : CategoryTheory.FreeMonoidalCategory C) → motive (T.tensor W) (X₂.tensor W) (f.whiskerRight W)),
  (match a, CategoryTheory.FreeMonoidalCategory.unit.tensor a, CategoryTheory.FreeMonoidalCategory.Hom.l_inv 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
    | .(T.tensor X), .(Y.tensor W), f.tensor g => h_9 T X Y W f g
    | .(T.tensor Y₁), .(T.tensor W), CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft T f => h_10 T Y₁ W f
    | .(T.tensor W), .(X₂.tensor W), f.whiskerRight W => h_11 T X₂ f W) =
    h_5 a