-- 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))))
    (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))))
have conv_rhs : 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))))
  (tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (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))))
Tactic: conv_rhs =>
      rw [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_assoc]
      dsimp
      rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_assoc]