-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_def : ∀ {C : Type u} (x x_1 : CategoryTheory.FreeMonoidalCategory C) (x_2 : x.Hom x_1),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux x_2 =
    match x, x_1, x_2 with
    | x, .(x), CategoryTheory.FreeMonoidalCategory.Hom.id .(x) => CategoryTheory.CategoryStruct.id x.normalizeObj'
    | .((X.tensor Y).tensor Z), .(X.tensor (Y.tensor Z)), CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z =>
      id
        (CategoryTheory.Discrete.natTrans fun x =>
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
                    Z).normalizeObj'.obj
              x))
    | .(X.tensor (Y.tensor Z)), .((X.tensor Y).tensor Z), CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z =>
      id
        (CategoryTheory.Discrete.natTrans fun x =>
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.MonoidalCategoryStruct.tensorObj X
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).normalizeObj'.obj
              x))
    | .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), a, CategoryTheory.FreeMonoidalCategory.Hom.l_hom .(a) =>
      id
        (CategoryTheory.Discrete.natTrans fun x =>
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.MonoidalCategoryStruct.tensorObj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C))
                    a).normalizeObj'.obj
              x))
    | a, .(CategoryTheory.FreeMonoidalCategory.unit.tensor a), CategoryTheory.FreeMonoidalCategory.Hom.l_inv .(a) =>
      id (CategoryTheory.Discrete.natTrans fun x => CategoryTheory.CategoryStruct.id (a.normalizeObj'.obj x))
    | .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), a, CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom .(a) =>
      id
        (CategoryTheory.Discrete.natTrans fun x =>
          CategoryTheory.CategoryStruct.id
            ((CategoryTheory.MonoidalCategoryStruct.tensorObj a
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                      (CategoryTheory.FreeMonoidalCategory C))).normalizeObj'.obj
              x))
    | a, .(a.tensor CategoryTheory.FreeMonoidalCategory.unit), CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv .(a) =>
      id (CategoryTheory.Discrete.natTrans fun x => CategoryTheory.CategoryStruct.id (a.normalizeObj'.obj x))
    | x, x_3, f.comp g =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.normalizeMapAux f)
        (CategoryTheory.FreeMonoidalCategory.normalizeMapAux g)
    | .(T.tensor X), .(Y.tensor W), f.tensor g =>
      CategoryTheory.Discrete.natTrans fun x =>
        match x with
        | { as := X_1 } =>
          CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.FreeMonoidalCategory.normalizeMapAux g).app { as := T.normalizeObj X_1 })
            (W.normalizeObj'.map ((CategoryTheory.FreeMonoidalCategory.normalizeMapAux f).app { as := X_1 }))
    | .(T.tensor Y₁), .(T.tensor W), CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft T f =>
      CategoryTheory.Discrete.natTrans fun x =>
        match x with
        | { as := X } => (CategoryTheory.FreeMonoidalCategory.normalizeMapAux f).app { as := T.normalizeObj X }
    | .(T.tensor W), .(X₂.tensor W), f.whiskerRight W =>
      CategoryTheory.Discrete.natTrans fun X =>
        W.normalizeObj'.map ((CategoryTheory.FreeMonoidalCategory.normalizeMapAux f).app X)