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

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm, assoc, ← μ_natural_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Functor.LaxMonoidal.μ_natural_left, CategoryTheory.Adjunction.homEquiv_naturality_left_symm