-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma pentagon (Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε) :
    Pentagon Y₁ Y₂ Y₃ Y₄

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
⊢ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

Tactic:
have : ((L').obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ (L').obj X₄ ≫
    (α_ ((L').obj X₁) ((L').obj X₂ ⊗ (L').obj X₃) ((L').obj X₄)).hom ≫
      (L').obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ (L').obj X₄ =
        (α_ ((L').obj X₁) ((L').obj (X₂ ⊗ X₃)) ((L').obj X₄)).hom :=
  pentagon_aux₂ _ _ _ (μ L W ε X₂ X₃).symm

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
        L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom =
    (α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫ (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom

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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom

Tactic:
refine Eq.trans ?_ (((((e₁.inv ⊗ e₂.inv) ⊗ e₃.inv) ⊗ e₄.inv) ≫= this =≫
  (e₁.hom ⊗ e₂.hom ⊗ e₃.hom ⊗ e₄.hom)).trans ?_)

Result:
case refine_1
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ Y₁ Y₂ Y₃).hom ▷ Y₄ ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ Y₁ ◁ (α_ Y₂ Y₃ Y₄).hom =
    (((e₁.inv ⊗ e₂.inv) ⊗ e₃.inv) ⊗ e₄.inv) ≫
      ((α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃)).hom ▷ L'.obj X₄ ≫
          (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫
            L'.obj X₁ ◁ (α_ (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ e₂.hom ⊗ e₃.hom ⊗ e₄.hom)

case refine_2
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (((e₁.inv ⊗ e₂.inv) ⊗ e₃.inv) ⊗ e₄.inv) ≫
      ((α_ (L'.obj X₁ ⊗ L'.obj X₂) (L'.obj X₃) (L'.obj X₄)).hom ≫
          (α_ (L'.obj X₁) (L'.obj X₂) (L'.obj X₃ ⊗ L'.obj X₄)).hom) ≫
        (e₁.hom ⊗ e₂.hom ⊗ e₃.hom ⊗ e₄.hom) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_a.e_a
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫
      L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom ≫
        (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv ≫ L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv) =
    L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫
      (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv ≫
        L'.obj (X₁ ⊗ X₂) ◁ (μ L W ε X₃ X₄).inv ≫
          (μ L W ε X₁ X₂).inv ▷ (L'.obj X₃ ⊗ L'.obj X₄) ≫
            (L'.obj X₁ ⊗ L'.obj X₂) ◁ (μ L W ε X₃ X₄).hom ≫
              (μ L W ε X₁ X₂).hom ▷ L'.obj (X₃ ⊗ X₄) ≫
                (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).hom ≫
                  L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom ≫
                    (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv ≫
                      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv)

Tactic:
simp only [← assoc]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_a.e_a
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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this :
  (L'.obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ L'.obj X₄ ≫
      (α_ (L'.obj X₁) (L'.obj X₂ ⊗ L'.obj X₃) (L'.obj X₄)).hom ≫ L'.obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ L'.obj X₄ =
    (α_ (L'.obj X₁) (L'.obj (X₂ ⊗ X₃)) (L'.obj X₄)).hom
⊢ ((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom) ≫ (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv) ≫
      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv) =
    ((((((((L'.map (α_ (X₁ ⊗ X₂) X₃ X₄).hom ≫ (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv) ≫
                    L'.obj (X₁ ⊗ X₂) ◁ (μ L W ε X₃ X₄).inv) ≫
                  (μ L W ε X₁ X₂).inv ▷ (L'.obj X₃ ⊗ L'.obj X₄)) ≫
                (L'.obj X₁ ⊗ L'.obj X₂) ◁ (μ L W ε X₃ X₄).hom) ≫
              (μ L W ε X₁ X₂).hom ▷ L'.obj (X₃ ⊗ X₄)) ≫
            (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).hom) ≫
          L'.map (α_ X₁ X₂ (X₃ ⊗ X₄)).hom) ≫
        (μ L W ε X₁ (X₂ ⊗ X₃ ⊗ X₄)).inv) ≫
      L'.obj X₁ ◁ ((μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv)