-- 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 Y : C
x : X ⟶ Y
x_1 : C
simp_rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    ((F ⋙ G).map x ▷ G.obj (F.obj x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
        (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
    (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)) ≫
      (F ⋙ G).map (x ▷ x_1))
simp_rw₁ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    (G.map (F.map x) ▷ G.obj (F.obj x_1) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
        (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
    (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.map (F.map (x ▷ x_1)))
simp_rw₂ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    (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.map x ▷ F.obj x_1) ≫ G.map (μ F Y x_1)))
    (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.map (F.map (x ▷ x_1)))
simp_rw₃ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    (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.map x ▷ F.obj x_1) ≫ G.map (μ F Y x_1)))
    (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.map (F.map (x ▷ x_1))))
simp_rw₄ :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X)) (G.obj (F.obj x_1)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    (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.map x ▷ F.obj x_1 ≫ μ F Y x_1)))
    (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 ≫ F.map (x ▷ x_1))))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj x_1) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1))
    ((F ⋙ G).map x ▷ (F ⋙ G).obj x_1 ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
        (μ G (F.obj Y) (F.obj x_1)) (G.map (μ F Y x_1)))
    (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)) ≫
      (F ⋙ G).map (x ▷ x_1))

Tactic:
simp_rw [comp_obj, F.comp_map, μ_natural_left_assoc, assoc, ← G.map_comp, μ_natural_left]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_left, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map