-- 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₃ : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj
        (Functor.obj (tensorBifunctor L W ε)
          (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁)) (Functor.obj L' X₂)))
        (Functor.obj L' X₃))
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁))
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₂)) (Functor.obj L' X₃))))
    (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (Iso.hom
              (Localization.associator L' L' L' L' L' L' W W W W W (F₁₂ := curriedTensor C) (curriedAssociatorNatIso C)
                (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)))
            (Functor.obj L' X₁))
          (Functor.obj L' X₂))
        (Functor.obj L' X₃) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj
          (Functor.obj (bifunctorComp₁₂Obj (tensorBifunctor L W ε) (tensorBifunctor L W ε) (Functor.obj L' X₁))
            (Functor.obj L' X₂))
          (Functor.obj L' X₃))
        (Functor.obj
          (Functor.obj (bifunctorComp₂₃Obj (tensorBifunctor L W ε) (tensorBifunctor L W ε) (Functor.obj L' X₁))
            (Functor.obj L' X₂))
          (Functor.obj L' X₃)))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (Iso.hom (μ L W ε X₁ X₂))) (Functor.obj L' X₃) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ≫
        Functor.map L' (Iso.hom (α_ X₁ X₂ X₃)) ≫
          Iso.inv (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) ≫
            Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁)) (Iso.inv (μ L W ε X₂ X₃)))
have rw : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε)
    (Functor.obj
      (Functor.obj (tensorBifunctor L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁)) (Functor.obj L' X₂)))
      (Functor.obj L' X₃))
    (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁))
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₂)) (Functor.obj L' X₃))))
  (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (tensorBifunctor L W ε)
          (Functor.obj
            (Functor.obj (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L') X₁)
            X₂))
        (Functor.obj L' X₃))
      (NatTrans.app
        (Functor.map (tensorBifunctor L W ε)
          (NatTrans.app
            (NatTrans.app
              (Iso.hom
                (Lifting₂.iso L' L' W W
                  (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                  (tensorBifunctor L W ε)))
              X₁)
            X₂))
        (Functor.obj L' X₃))
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L')
            (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) X₂))
          X₃)
        (NatTrans.app
          (NatTrans.app
            (Iso.hom
              (Lifting₂.iso L' L' W W
                (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                (tensorBifunctor L W ε)))
            (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) X₂))
          X₃)
        (Functor.map L' (NatTrans.app (NatTrans.app (NatTrans.app (Iso.hom (curriedAssociatorNatIso C)) X₁) X₂) X₃) ≫
          CategoryStruct.comp (Y :=
            Functor.obj
              (Functor.obj
                (Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ (LocalizedMonoidal L W ε)) L') L')
                  (tensorBifunctor L W ε))
                X₁)
              (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₂) X₃))
            (NatTrans.app
                (NatTrans.app
                  (Iso.inv
                    (Lifting₂.iso L' L' W W
                      (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                      (tensorBifunctor L W ε)))
                  X₁)
                (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₂) X₃) :
              Quiver.Hom (V := LocalizedMonoidal L W ε)
                (Functor.obj
                  (Functor.obj
                    (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L') X₁)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₂) X₃))
                (Functor.obj
                  (Functor.obj
                    (Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ (LocalizedMonoidal L W ε)) L') L')
                      (tensorBifunctor L W ε))
                    X₁)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₂) X₃)))
            (Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁))
                (NatTrans.app
                  (NatTrans.app
                    (Iso.inv
                      (Lifting₂.iso L' L' W W
                        (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                        (tensorBifunctor L W ε)))
                    X₂)
                  X₃) :
              Quiver.Hom (V := LocalizedMonoidal L W ε)
                (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁))
                  (Functor.obj L' (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₂) X₃)))
                (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁))
                  (Functor.obj
                    (Functor.obj
                      (Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ (LocalizedMonoidal L W ε)) L') L')
                        (tensorBifunctor L W ε))
                      X₂)
                    X₃))))) :
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj
        (Functor.obj (tensorBifunctor L W ε)
          (Functor.obj
            (Functor.obj
              (Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ (LocalizedMonoidal L W ε)) L') L')
                (tensorBifunctor L W ε))
              X₁)
            X₂))
        (Functor.obj L' X₃))
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁))
        (Functor.obj
          (Functor.obj
            (Functor.obj (Functor.obj (Functor.obj (Functor.whiskeringLeft₂ (LocalizedMonoidal L W ε)) L') L')
              (tensorBifunctor L W ε))
            X₂)
          X₃)))
  (NatTrans.app (Functor.map (tensorBifunctor L W ε) (Iso.hom (μ L W ε X₁ X₂))) (Functor.obj L' X₃) ≫
    Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ≫
      Functor.map L' (Iso.hom (α_ X₁ X₂ X₃)) ≫
        Iso.inv (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) ≫
          Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X₁)) (Iso.inv (μ L W ε X₂ X₃)))
Tactic: rw [Localization.associator_hom_app_app_app]