-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε}
    (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
    ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, 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:
rw [h₁, assoc, reassoc_of% h₂, reassoc_of% h₃]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, 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 only [monoidalCategoryStruct, Functor.map_comp, assoc]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, 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₃)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, 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₃
⊢ ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)

Tactic:
have h₁ := (((associator L W ε).hom.app Y₁).app Y₂).naturality f₃

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, 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₃
⊢ ((f₁ ⊗ f₂) ⊗ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom = (α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ f₂ ⊗ f₃)