-- 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.e_a.e_a.e_a.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₁ ⊗ 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

Tactic:
simp only [← cancel_mono (μ L W ε (X₁ ⊗ X₂) (X₃ ⊗ X₄)).inv, assoc, id_comp,
  whisker_exchange_assoc, ← whiskerRight_comp_assoc,
  Iso.inv_hom_id, whiskerRight_id, ← whiskerLeft_comp,
  whiskerLeft_id]

Result:
no goals

Proof state:
case 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₂
⊢ Pentagon Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₃, ⟨e₃⟩⟩ : ∃ X₃, Nonempty ((L').obj X₃ ≅ Y₃) := ⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩

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

Tactic:
simp only [assoc, ← whiskerRight_comp_assoc, Iso.inv_hom_id, comp_id, μ_natural_left_assoc,
  id_tensorHom, ← whiskerLeft_comp, Iso.inv_hom_id_assoc]

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 W ε X₁ X₂).hom ▷ L'.obj X₃ ≫ (μ L W ε (X₁ ⊗ X₂) X₃).hom) ▷ L'.obj X₄ ≫
      (μ L W ε ((X₁ ⊗ X₂) ⊗ X₃) X₄).hom ≫
        L'.map ((α_ X₁ X₂ X₃).hom ▷ X₄) ≫
          L'.map (α_ X₁ (X₂ ⊗ X₃) X₄).hom ≫
            (μ L W ε X₁ ((X₂ ⊗ X₃) ⊗ X₄)).inv ≫
              L'.obj X₁ ◁ (L'.map (α_ X₂ X₃ X₄).hom ≫ (μ L W ε X₂ (X₃ ⊗ X₄)).inv ≫ L'.obj X₂ ◁ (μ L W ε X₃ X₄).inv) =
    (μ L W ε X₁ X₂).hom ▷ L'.obj X₃ ▷ L'.obj X₄ ≫
      ((μ L W ε (X₁ ⊗ X₂) X₃).hom ⊗ 𝟙 (L'.obj 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₁ ⊗ 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)