-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
simp :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ G.obj Z) ≫
          δ F (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z) ≫
            (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
⊢ Eq.{v₂ + 1} (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (((Equiv.symm
              (adj.homEquiv
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z))
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) :
            Equiv.{v₁ + 1, v₂ + 1}
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
                G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
                tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) :
          (a : (G.obj X ⊗ G.obj Y) ⊗ G.obj Z ⟶ G.obj (X ⊗ Y ⊗ Z)) → F.obj ((G.obj X ⊗ G.obj Y) ⊗ G.obj Z) ⟶ X ⊗ Y ⊗ Z)
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z))
          (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) :
                  Equiv.{v₂ + 1, v₁ + 1}
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y) ⟶
                      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))) :
                (a : F.obj (G.obj X ⊗ G.obj Y) ⟶ X ⊗ Y) → G.obj X ⊗ G.obj Y ⟶ G.obj (X ⊗ Y))
              (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷
            G.obj Z)
          (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z))
                    (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) :
                  Equiv.{v₂ + 1, v₁ + 1}
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z)) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z)
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z) ⟶
                      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z))) :
                (a : F.obj (G.obj (X ⊗ Y) ⊗ G.obj Z) ⟶ (X ⊗ Y) ⊗ Z) → G.obj (X ⊗ Y) ⊗ G.obj Z ⟶ G.obj ((X ⊗ Y) ⊗ Z))
              (δ F (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z) ≫
                (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z)) ≫
            G.map (Iso.hom (α_ X Y Z)))) :
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
        tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (((Equiv.symm
              (adj.homEquiv
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z))
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) :
            Equiv.{v₁ + 1, v₂ + 1}
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
                G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
                tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) :
          (a : (G.obj X ⊗ G.obj Y) ⊗ G.obj Z ⟶ G.obj (X ⊗ Y ⊗ Z)) → F.obj ((G.obj X ⊗ G.obj Y) ⊗ G.obj Z) ⟶ X ⊗ Y ⊗ Z)
        (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
            (G.obj X ◁
              ((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z) :
                    Equiv.{v₂ + 1, v₁ + 1}
                      (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ⟶
                        tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)
                      (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z) ⟶
                        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) :
                  (a : F.obj (G.obj Y ⊗ G.obj Z) ⟶ Y ⊗ Z) → G.obj Y ⊗ G.obj Z ⟶ G.obj (Y ⊗ Z))
                (δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app Y ⊗ₘ adj.counit.app Z)))
            (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
                    (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) :
                  Equiv.{v₂ + 1, v₁ + 1}
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ⟶
                      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))) :
                (a : F.obj (G.obj X ⊗ G.obj (Y ⊗ Z)) ⟶ X ⊗ Y ⊗ Z) → G.obj X ⊗ G.obj (Y ⊗ Z) ⟶ G.obj (X ⊗ Y ⊗ Z))
              (δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))))) :
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
        tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))

Tactic:
simp only [homEquiv_unit, comp_obj, map_comp, comp_whiskerRight, assoc, homEquiv_counit,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
      MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Adjunction.counit_naturality_assoc, CategoryTheory.Adjunction.left_triangle_components_assoc