-- 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 :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
          (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)))
        (Functor.obj L' X₄))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
          (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) (Functor.obj L' X₄))))
    ((Functor.obj L' X₁ ◁ Iso.inv (μ L W ε X₂ X₃)) ▷ Functor.obj L' X₄ ≫
      Iso.hom
          (α_ (Functor.obj L' X₁)
            (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 (μ L W ε X₂ X₃) ▷ Functor.obj L' X₄)
    (Iso.hom (α_ (Functor.obj L' X₁) (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) (Functor.obj L' X₄)))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
          (Functor.obj L' X₃))
        (Functor.obj L' X₄))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₂)
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃) (Functor.obj L' X₄)))))
    (Iso.hom (μ L W ε X₁ X₂) ▷ Functor.obj L' X₃ ▷ Functor.obj L' X₄ ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ▷ Functor.obj L' X₄ ≫
        Functor.map L' (Iso.hom (α_ X₁ X₂ X₃)) ▷ Functor.obj L' X₄ ≫
          Iso.inv (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) ▷ Functor.obj L' X₄ ≫
            (Iso.hom (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) ▷ Functor.obj L' X₄ ≫
                Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) X₄) ≫
                  Functor.map L' (Iso.hom (α_ X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃) X₄)) ≫
                    Iso.inv
                        (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃) X₄)) ≫
                      (𝟙 (Functor.obj L' X₁) ⊗ₘ Iso.inv (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃) X₄))) ≫
              Functor.obj L' X₁ ◁
                (Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃) X₄) ≫
                  Functor.map L' (Iso.hom (α_ X₂ X₃ X₄)) ≫
                    Iso.inv (μ L W ε X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
                      (𝟙 (Functor.obj L' X₂) ⊗ₘ Iso.inv (μ L W ε X₃ X₄))))
    ((Iso.hom (μ L W ε X₁ X₂) ▷ Functor.obj L' X₃ ▷ Functor.obj L' X₄ ≫
        ((Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ⊗ₘ 𝟙 (Functor.obj L' X₄)) ≫
            Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) X₄) ≫
              Functor.map L' (Iso.hom (α_ (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃ X₄)) ≫
                Iso.inv (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
                  (𝟙 (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) ⊗ₘ Iso.inv (μ L W ε X₃ X₄))) ≫
          Iso.inv (μ L W ε X₁ X₂) ▷
            tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃) (Functor.obj L' X₄)) ≫
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) ◁
          Iso.hom (μ L W ε X₃ X₄) ≫
        ((Iso.hom (μ L W ε X₁ X₂) ⊗ₘ 𝟙 (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄))) ≫
            Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
              Functor.map L' (Iso.hom (α_ X₁ X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄))) ≫
                Iso.inv (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄))) ≫
                  (𝟙 (Functor.obj L' X₁) ⊗ₘ Iso.inv (μ L W ε X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)))) ≫
          Functor.obj L' X₁ ◁ Functor.obj L' X₂ ◁ Iso.inv (μ L W ε X₃ X₄))
have simp : Eq (α :=
  Quiver.Hom (V := LocalizedMonoidal L W ε)
    (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂))
        (Functor.obj L' X₃))
      (Functor.obj L' X₄))
    (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₂)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃) (Functor.obj L' X₄)))))
  ((Iso.hom (μ L W ε X₁ X₂) ▷ Functor.obj L' X₃ ≫ Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃)) ▷
      Functor.obj L' X₄ ≫
    Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) X₄) ≫
      Functor.map L' (Iso.hom (α_ X₁ X₂ X₃) ▷ X₄) ≫
        Functor.map L' (Iso.hom (α_ X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃) X₄)) ≫
          Iso.inv (μ L W ε X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃) X₄)) ≫
            Functor.obj L' X₁ ◁
              (Functor.map L' (Iso.hom (α_ X₂ X₃ X₄)) ≫
                Iso.inv (μ L W ε X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
                  Functor.obj L' X₂ ◁ Iso.inv (μ L W ε X₃ X₄)))
  (Iso.hom (μ L W ε X₁ X₂) ▷ Functor.obj L' X₃ ▷ Functor.obj L' X₄ ≫
    (Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ⊗ₘ 𝟙 (Functor.obj L' X₄)) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) X₄) ≫
        Functor.map L' (Iso.hom (α_ (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃ X₄)) ≫
          Iso.inv (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
            Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ◁ Iso.inv (μ L W ε X₃ X₄) ≫
              Iso.inv (μ L W ε X₁ X₂) ▷
                  tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₃)
                    (Functor.obj L' X₄) ≫
                tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
                      (Functor.obj L' X₂) ◁
                    Iso.hom (μ L W ε X₃ X₄) ≫
                  (Iso.hom (μ L W ε X₁ X₂) ⊗ₘ 𝟙 (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄))) ≫
                    Iso.hom
                        (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
                      Functor.map L' (Iso.hom (α_ X₁ X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄))) ≫
                        Iso.inv
                            (μ L W ε X₁
                              (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄))) ≫
                          Functor.obj L' X₁ ◁
                            (Iso.inv (μ L W ε X₂ (tensorObj.{v_1, u_1} (𝒞 := inst) X₃ X₄)) ≫
                              Functor.obj L' X₂ ◁ Iso.inv (μ L W ε X₃ X₄)))
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]