-- 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
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ Y
h₁ :
  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' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L'
        (tensorObj.{v_1, u_1} (𝒞 := inst) X'
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      Functor.obj L' X' ◁ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫
        Iso.hom (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    ((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
h₂ :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
      (Functor.obj L' Y'))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
    (Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ Y')))
h₃ :
  ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
        Functor.obj L' X' ◁
            (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
              tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ◁ e₂.hom ≫
                Iso.hom (λ_ Y)) ≫
          e₁.hom ▷ Y =
    ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
            (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ◁
          e₂.hom ≫
        (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X'))) ▷ Y ≫ e₁.hom ▷ Y
this :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y))
    (((e₁.symm.hom ⊗ₘ ε.symm.hom) ⊗ₘ e₂.symm.hom) ≫
      Iso.hom (α_ (Functor.obj L' X') (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
        (e₁.symm.inv ⊗ₘ ε.symm.inv ⊗ₘ e₂.symm.inv))
    (Iso.hom (α_ X (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y))
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (α_ X (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)
have simp : ((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
    Iso.hom (α_ (Functor.obj L' X') (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y)) =
  Iso.hom (ρ_ X) ▷ Y
Tactic: simp only [← this, Iso.symm_hom, Iso.symm_inv, assoc,
    ← id_tensorHom, ← tensor_comp, comp_id]