-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Category (goal)
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))
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have 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
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]