-- 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
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
X Y Z : C
rw :
  Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₁ :
  (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₂ :
  (h.μIso X Y).hom ▷ F.obj Z ≫ (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    (h.μIso X Y).hom ▷ F.obj Z ≫
      Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        F.map (Iso.hom (α_ X Y Z)) ≫
          Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₃ :
  Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    (h.μIso X Y).hom ▷ F.obj Z ≫
      Iso.hom (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        F.map (Iso.hom (α_ X Y Z)) ≫
          Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₄ :
  Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      F.obj X ◁ (h.μIso Y Z).hom ≫
        Iso.hom (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
          Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₅ :
  Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ (h.μIso Y Z).hom ≫ F.obj X ◁ (h.μIso Y Z).inv
rw₆ :
  Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
rw₇ rw₈ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z))) (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
⊢ Iso.inv (h.μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
      (h.μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
    F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (h.μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (h.μIso Y Z).inv

Tactic:
rw [← cancel_epi (h.μIso (X ⊗ Y) Z).hom, Iso.hom_inv_id_assoc,
      ← cancel_epi ((h.μIso X Y).hom ▷ F.obj Z), hom_inv_whiskerRight_assoc,
      associativity_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv, comp_id]

Premises used: CategoryTheory.Functor.CoreMonoidal.μIso, CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc, CategoryTheory.Functor.CoreMonoidal.associativity_assoc, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj