-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁
      (hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst))
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y)
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)))
rw₂ :
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
    hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
      tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
rw₃ :
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
      hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
    hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
      hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫
          tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
rw₄ :
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
      hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
    hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y)) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
rw₅ :
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
      hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X) Y) ≫
        tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X) ▷ Y =
    hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorObj.{v, u} (𝒞 := inst) X Y
rw₆ :
  hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ▷ Y ≫
      (tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X)) ▷ Y ≫ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) =
    hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorObj.{v, u} (𝒞 := inst) X Y
rw₇ :
  (hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) X) ≫
          tensorUnit.{v, u} C (𝒞 := inst) ◁ hom (λ_ X)) ▷
        Y ≫
      hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) =
    hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorObj.{v, u} (𝒞 := inst) X Y
rw₈ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst)
        (tensorObj.{v, u} (𝒞 := inst)
          (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X)
        Y ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ X ▷ Y ≫ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y))
    (hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorObj.{v, u} (𝒞 := inst) X Y)
rw₉ rw₁₀ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst)
        (tensorObj.{v, u} (𝒞 := inst)
          (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X)
        Y ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorObj.{v, u} (𝒞 := inst) X Y))
    (hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorObj.{v, u} (𝒞 := inst) X Y)
    (hom (α_ (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) X Y) ≫
      hom (ρ_ (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorObj.{v, u} (𝒞 := inst) X Y)
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))

Tactic:
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
      cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
      comp_whiskerRight_assoc, triangle, associator_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.associator_naturality_left, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategory.whiskerLeft_iff, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.triangle, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.MonoidalCategory.pentagon_assoc