-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).obj Y₂)).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
h₂ :
  NatTrans.app (Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂)) X₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂).app X₃ ≫
      (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃)
h₃ :
  Eq (α :=
    (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) X₁).obj X₂)).obj X₃ ⟶
      (Functor.obj (tensorBifunctor L W ε) Y₁).obj ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂)) X₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂).app X₃)
    (((NatTrans.app (Iso.hom (associator L W ε)) X₁).app X₂).app X₃ ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃))
rw :
  (NatTrans.app (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂)) X₃ ≫
        NatTrans.app (Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂)) X₃) ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃) =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁).app X₂).app X₃ ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
          (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
rw₁ :
  NatTrans.app (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂)) X₃ ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂)) X₃ ≫
        ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
          (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃) =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁).app X₂).app X₃ ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
          (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
⊢ (NatTrans.app (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂)) X₃ ≫
        NatTrans.app (Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂)) X₃) ≫
      (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).obj Y₂)).map f₃ ≫
        ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁).app X₂).app X₃ ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
          (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
have rw₂ : NatTrans.app (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂)) X₃ ≫
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂).app X₃ ≫
      (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃) =
  ((NatTrans.app (Iso.hom (associator L W ε)) X₁).app X₂).app X₃ ≫
    NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
      (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
Tactic: rw [h₁, assoc, reassoc_of% h₂, reassoc_of% h₃]