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₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      (((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃
h₂ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂ ≫
          ((associator L W ε).hom.app Y₁).app Y₂).app
      X₃ =
    (((associator L W ε).hom.app Y₁).app X₂ ≫
          ((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂).app
      X₃
h₃ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).map f₁ ≫ (associator L W ε).hom.app Y₁).app
          X₂).app
      X₃ =
    (((associator L W ε).hom.app X₁ ≫ (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).map f₁).app
          X₂).app
      X₃
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)

Tactic:
simp +instances only [monoidalCategoryStruct, Functor.map_comp, assoc]

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₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₁ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃ ≫
      (((associator L W ε).hom.app Y₁).app Y₂).app Y₃ =
    (((associator L W ε).hom.app Y₁).app Y₂).app X₃ ≫
      (((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).obj Y₂).map f₃
h₂ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂ ≫
          ((associator L W ε).hom.app Y₁).app Y₂).app
      X₃ =
    (((associator L W ε).hom.app Y₁).app X₂ ≫
          ((bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).obj Y₁).map f₂).app
      X₃
h₃ :
  (((bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).map f₁ ≫ (associator L W ε).hom.app Y₁).app
          X₂).app
      X₃ =
    (((associator L W ε).hom.app X₁ ≫ (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)).map f₁).app
          X₂).app
      X₃
⊢ ((tensorBifunctor L W ε).map (((tensorBifunctor L W ε).map f₁).app X₂) ≫
            (tensorBifunctor L W ε).map (((tensorBifunctor L W ε).obj Y₁).map f₂)).app
        X₃ ≫
      ((tensorBifunctor L W ε).obj (((tensorBifunctor L W ε).obj Y₁).obj Y₂)).map f₃ ≫
        ((((associator L W ε).app Y₁).app Y₂).app Y₃).hom =
    ((((associator L W ε).app X₁).app X₂).app X₃).hom ≫
      ((tensorBifunctor L W ε).map f₁).app (((tensorBifunctor L W ε).obj X₂).obj X₃) ≫
        ((tensorBifunctor L W ε).obj Y₁).map (((tensorBifunctor L W ε).map f₂).app X₃) ≫
          ((tensorBifunctor L W ε).obj Y₁).map (((tensorBifunctor L W ε).obj Y₂).map f₃)