-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
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
⊢ 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))))
have conv_lhs : 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))))
  (tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
          G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
              G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
        G.obj (F.obj Z) ≫
      μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
        G.map (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))))
Tactic: conv_lhs =>
      rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_assoc]
      dsimp
      rw [← comp_whiskerRight_assoc]