-- 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.OplaxMonoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    ((F.map (Iso.inv (α_ X Y 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)))
rw₂ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y 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)))
rw₄ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z)) ≫
      F.map (Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₅ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    ((F.map (Iso.inv (α_ X Y Z)) ≫ F.map (Iso.hom (α_ X Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₆ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (α_ X Y Z)) ≫ δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₇ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (F.map (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₈ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
      δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
rw₉ rw₁₀ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
    (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.obj X ◁ δ F Y Z)
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj 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.map (Iso.inv (α_ X Y Z)) ≫ δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ δ F X Y ▷ F.obj Z)

Tactic:
rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
    ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, id_comp]

Premises used: CategoryTheory.Functor.OplaxMonoidal.associativity, CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp