-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.hom (α_ X Y Z)) ≫ F.map (Iso.inv (α_ X Y Z)))
    (F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (F.obj X ◁ δ F Y Z ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₁ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (F.obj X ◁ δ F Y Z ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
rw₂ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
        (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
        (δ F X Y ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (F.obj X ◁ δ F Y Z ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₃ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
        (δ F X Y ▷ F.obj Z ≫
          Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
          (F.obj X ◁ δ F Y Z ≫
            Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
              μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₄ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
            (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
            (F.obj X ◁ δ F Y Z ≫
              Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₅ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
            (F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
            (CategoryStruct.comp (Y :=
              tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
              (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
              (F.obj X ◁ δ F Y Z ≫
                Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                  μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₆ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) (F.obj X ◁ μ F Y Z)
            (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
              (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
              (CategoryStruct.comp (Y :=
                tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
                (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
                (F.obj X ◁ δ F Y Z ≫
                  Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
                    μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))))
rw₇ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) (F.obj X ◁ μ F Y Z)
            (μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
              F.map (Iso.inv (α_ X Y Z)) ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
                  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
                  (CategoryStruct.comp (Y :=
                    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
                    (δ F X Y ▷ F.obj Z) (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))))
rw₈ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          F.obj X ◁ μ F Y Z ≫
            μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
              F.map (Iso.inv (α_ X Y Z)) ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
                  (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₉ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          F.obj X ◁ μ F Y Z ≫
            μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
              F.map (Iso.inv (α_ X Y Z)) ≫
                𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
rw₁₀ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (Iso.inv (α_ X Y Z)))
rw₁₁ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
          Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
rw₁₂ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
        (δ F X Y ▷ F.obj Z) (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
rw₁₃ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
rw₁₄ rw₁₅ :
  Eq.{v₂ + 1} (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
    (𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (F.map (Iso.inv (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
      (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
      (F.obj X ◁ δ F Y Z ≫
        Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))

Tactic:
rw [← cancel_epi (F.map (α_ X Y Z).hom), Iso.map_hom_inv_id, map_associator,
    assoc, assoc, assoc, assoc, OplaxMonoidal.associativity_inv_assoc,
    whiskerRight_δ_μ_assoc, δ_μ, comp_id, LaxMonoidal.associativity_inv,
    Iso.hom_inv_id_assoc, whiskerRight_δ_μ_assoc, δ_μ]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.Functor.Monoidal.map_associator, CategoryTheory.Iso.map_hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Functor.LaxMonoidal.associativity_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc, CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc