Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ : C
⊢ ((tensorBifunctor L W ε).map
            (((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).hom.app
                  X₁).app
              X₂)).app
        (L'.obj X₃) ≫
      ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                    (tensorBifunctor L W ε)).hom.app
              (((curriedTensor C).obj X₁).obj X₂)).app
          X₃ ≫
        L'.map ((((curriedAssociatorNatIso C).hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).inv.app
                  X₁).app
              (((curriedTensor C).obj X₂).obj X₃) ≫
            ((tensorBifunctor L W ε).obj (L'.obj X₁)).map
              (((Lifting₂.iso L' L' W W
                          (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                          (tensorBifunctor L W ε)).inv.app
                    X₂).app
                X₃) =
    ((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ : C
⊢ ((tensorBifunctor L W ε).map
            (((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).hom.app
                  X₁).app
              X₂)).app
        (L'.obj X₃) ≫
      ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                    (tensorBifunctor L W ε)).hom.app
              (((curriedTensor C).obj X₁).obj X₂)).app
          X₃ ≫
        L'.map ((((curriedAssociatorNatIso C).hom.app X₁).app X₂).app X₃) ≫
          ((Lifting₂.iso L' L' W W (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                        (tensorBifunctor L W ε)).inv.app
                  X₁).app
              (((curriedTensor C).obj X₂).obj X₃) ≫
            ((tensorBifunctor L W ε).obj (L'.obj X₁)).map
              (((Lifting₂.iso L' L' W W
                          (curriedTensor C ⋙ (Functor.whiskeringRight C C (LocalizedMonoidal L W ε)).obj L')
                          (tensorBifunctor L W ε)).inv.app
                    X₂).app
                X₃) =
    ((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv