-- 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
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.LaxMonoidal
inst_8 : G.LaxMonoidal
x x_1 x_2 : C
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
          (G.obj (F.obj x_2)))
        (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2)) (G.map (μ F x x_1) ▷ G.obj (F.obj x_2)) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        G.map (F.map (Iso.hom (α_ x x_1 x_2))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
simp_rw₁ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (G.map (μ F x x_1) ▷ G.obj (F.obj x_2) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
simp_rw₂ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2)))
        (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2))
        (G.map (μ F x x_1 ▷ F.obj x_2) ≫
          G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
simp_rw₃ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2)))
        (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2))
        (G.map (μ F x x_1 ▷ F.obj x_2) ≫
          G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      CategoryStruct.comp (Y :=
          tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x))
            (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
          (G.obj (F.obj x) ◁ μ G (F.obj x_1) (F.obj x_2)) (G.obj (F.obj x) ◁ G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
simp_rw₄ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2)))
        (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2))
        (G.map (μ F x x_1 ▷ F.obj x_2) ≫
          G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x))
          (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
        (G.obj (F.obj x) ◁ μ G (F.obj x_1) (F.obj x_2))
        (G.obj (F.obj x) ◁ G.map (μ F x_1 x_2) ≫
          CategoryStruct.comp (Y :=
            G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
            (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
            (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))))
simp_rw₅ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2)))
        (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2))
        (G.map (μ F x x_1 ▷ F.obj x_2) ≫
          G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x))
          (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
        (G.obj (F.obj x) ◁ μ G (F.obj x_1) (F.obj x_2))
        (CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
          (μ G (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
          (G.map (F.obj x ◁ μ F x_1 x_2) ≫ G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))))
simp_rw₆ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2)))
        (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2))
        (G.map (μ F x x_1 ▷ F.obj x_2) ≫
          G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ≫ G.map (F.map (Iso.hom (α_ x x_1 x_2))))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2) ≫
        G.map (Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2))) ≫
          G.map (F.obj x ◁ μ F x_1 x_2) ≫ G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
simp_rw₇ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2)))
        (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2))
        (G.map
          (μ F x x_1 ▷ F.obj x_2 ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2 ≫ F.map (Iso.hom (α_ x x_1 x_2))))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
        (G.obj (F.obj x_2)))
      (μ G (F.obj x) (F.obj x_1) ▷ G.obj (F.obj x_2))
      (μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)) (F.obj x_2) ≫
        G.map
          (Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2)) ≫
            F.obj x ◁ μ F x_1 x_2 ≫ μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj x)) (G.obj (F.obj x_1)))
        (G.obj (F.obj x_2)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1)))
          (μ G (F.obj x) (F.obj x_1)) (G.map (μ F x x_1)) ▷
        G.obj (F.obj x_2) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2)))
          (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (F.obj x_2))
          (G.map (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2)) ≫
        G.map (F.map (Iso.hom (α_ x x_1 x_2))))
    (Iso.hom (α_ (G.obj (F.obj x)) (G.obj (F.obj x_1)) (G.obj (F.obj x_2))) ≫
      G.obj (F.obj x) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
            (μ G (F.obj x_1) (F.obj x_2)) (G.map (μ F x_1 x_2)) ≫
        CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))
          (μ G (F.obj x) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2)))
          (G.map (μ F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2))))

Tactic:
simp_rw [comp_whiskerRight, assoc, μ_natural_left_assoc, MonoidalCategory.whiskerLeft_comp,
      assoc, μ_natural_right_assoc, ← associativity_assoc, ← G.map_comp, associativity]

Premises used: CategoryTheory.Functor.LaxMonoidal.associativity_assoc, CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc, CategoryTheory.Functor.LaxMonoidal.associativity, CategoryTheory.Functor.map_comp