-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
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₃))))
    (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:
rfl