-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma associator_hom_app (X₁ X₂ X₃ : C) :
    (α_ ((L').obj X₁) ((L').obj X₂) ((L').obj X₃)).hom =
      ((μ L W ε _ _).hom ⊗ 𝟙 _) ≫ (μ L W ε _ _).hom ≫ (L').map (α_ X₁ X₂ X₃).hom ≫
        (μ L W ε  _ _).inv ≫ (𝟙 _ ⊗ (μ L W ε  _ _).inv)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, 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
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj X₃) =
    (((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
        ((tensorBifunctor L W ε).obj (L'.obj (X₁ ⊗ X₂))).map (𝟙 (L'.obj X₃))) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫
            ((tensorBifunctor L W ε).map (𝟙 (L'.obj X₁))).app (L'.obj (X₂ ⊗ X₃)) ≫
              ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv

Tactic:
simp only [Functor.map_id, comp_id, NatTrans.id_app, id_comp]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, 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
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj 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

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, 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 ⋙ (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 ⋙ (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 ⋙ (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 ⋙ (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:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, 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
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj 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:
rw [Localization.associator_hom_app_app_app]

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

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, 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
⊢ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom =
    ((μ L W ε X₁ X₂).hom ⊗ 𝟙 (L'.obj X₃)) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫ (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫ (𝟙 (L'.obj X₁) ⊗ (μ L W ε X₂ X₃).inv)

Tactic:
dsimp [monoidalCategoryStruct, associator]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, 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
⊢ (((Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
                    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)).hom.app
              (L'.obj X₁)).app
          (L'.obj X₂)).app
      (L'.obj X₃) =
    (((tensorBifunctor L W ε).map (μ L W ε X₁ X₂).hom).app (L'.obj X₃) ≫
        ((tensorBifunctor L W ε).obj (L'.obj (X₁ ⊗ X₂))).map (𝟙 (L'.obj X₃))) ≫
      (μ L W ε (X₁ ⊗ X₂) X₃).hom ≫
        L'.map (α_ X₁ X₂ X₃).hom ≫
          (μ L W ε X₁ (X₂ ⊗ X₃)).inv ≫
            ((tensorBifunctor L W ε).map (𝟙 (L'.obj X₁))).app (L'.obj (X₂ ⊗ X₃)) ≫
              ((tensorBifunctor L W ε).obj (L'.obj X₁)).map (μ L W ε X₂ X₃).inv