-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
this :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
refine_2 :
  (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      Iso.hom
          (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
            (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
        Iso.hom
            (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                (Functor.obj L' X₄))) ≫
          (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
refine_2₁ :
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      ((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫
        Iso.hom
            (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                (Functor.obj L' X₄))) ≫
          (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
refine_2₂ :
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄)) ≫
        (e₁.inv ⊗ₘ e₂.inv ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫ (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
refine_2₃ :
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄)) ≫
        (e₁.inv ≫ e₁.hom ⊗ₘ (e₂.inv ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫ (e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
refine_2₄ :
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄)) ≫
        (𝟙 Y₁ ⊗ₘ (e₂.inv ⊗ₘ e₃.inv ⊗ₘ e₄.inv) ≫ (e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
⊢ (((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫
      (Iso.hom
            (α_
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
              (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
          Iso.hom
            (α_ (Functor.obj L' X₁) (Functor.obj L' X₂)
              (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                (Functor.obj L' X₄)))) ≫
        (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
have refine_2₅ : Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
    Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄)) ≫
      (𝟙 Y₁ ⊗ₘ e₂.inv ≫ e₂.hom ⊗ₘ (e₃.inv ⊗ₘ e₄.inv) ≫ (e₃.hom ⊗ₘ e₄.hom)) =
  Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
    Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))
Tactic: rw [assoc, associator_naturality_assoc, associator_naturality_assoc,
        ← tensor_comp, e₁.inv_hom_id, ← tensor_comp, e₂.inv_hom_id, ← tensor_comp,
        e₃.inv_hom_id, e₄.inv_hom_id, id_tensorHom_id, id_tensorHom_id, id_tensorHom_id, comp_id]