-- 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))
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)
⊢ hom (λ_ X) ▷ Y = hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have 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)
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]