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

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm,
      Equiv.apply_symm_apply, Equiv.apply_symm_apply, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, Equiv.apply_symm_apply, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv_naturality_left_symm