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

Tactic:
h₁,

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