-- 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)
        (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))))
        (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
    ((X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
    ((Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))) ▷
      tensorUnit.{v, u} C (𝒞 := inst))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst)
        (tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))))
        (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
    ((X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
    (Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
      hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X
        (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst)))
          (tensorUnit.{v, u} C (𝒞 := inst))) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
    (Iso.inv
        (α_ X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      (X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
    (Iso.inv
        (α_ X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
⊢ X ◁ hom (ρ_ Y) = Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))
have rw₃ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) X
      (tensorObj.{v, u} (𝒞 := inst) Y
        (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) (tensorUnit.{v, u} C (𝒞 := inst)))
  (X ◁ Iso.inv (α_ Y (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
    Iso.inv
        (α_ X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      (X ◁ hom (ρ_ Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
  (X ◁ Iso.inv (α_ Y (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
    Iso.inv
        (α_ X (tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst))) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫
        hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) ▷ tensorUnit.{v, u} C (𝒞 := inst))
Tactic: rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ←
      cancel_epi (X ◁ (α_ _ _ _).inv), pentagon_inv_assoc, triangle_assoc_comp_right, ←
      associator_inv_naturality_middle, ← whiskerLeft_comp_assoc, triangle_assoc_comp_right,
      associator_inv_naturality_right]