∀ (C : Type u) (x : CategoryTheory.FreeMonoidalCategory C)
  (x_1 : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C x x_1 =
    match x, x_1 with
    | CategoryTheory.FreeMonoidalCategory.of a, x =>
      CategoryTheory.Iso.refl
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
          (CategoryTheory.FreeMonoidalCategory.of a))
    | CategoryTheory.FreeMonoidalCategory.unit, x =>
      CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusionObj x)
    | X.tensor Y, n =>
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusionObj n) X
            Y).symm ≪≫
        CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n)
            Y ≪≫
          CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C Y (X.normalizeObj n)