-- 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)
        (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))
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))
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))
    (Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      Iso.inv
          (α_ (tensorObj.{v, u} (𝒞 := inst) 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₅ :
  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) =
    Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      tensorObj.{v, u} (𝒞 := inst) X Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))
rw₆ :
  X ◁ Iso.inv (α_ Y (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
      X ◁ hom (ρ_ Y) ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) =
    Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      tensorObj.{v, u} (𝒞 := inst) X Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))
rw₇ :
  X ◁
        (Iso.inv (α_ Y (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst))) ≫
          hom (ρ_ Y) ▷ tensorUnit.{v, u} C (𝒞 := inst)) ≫
      Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) =
    Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      tensorObj.{v, u} (𝒞 := inst) X Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))
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 ◁ Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))))
    (Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      tensorObj.{v, u} (𝒞 := inst) X Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst))))
rw₉ 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)))
    (Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      tensorObj.{v, u} (𝒞 := inst) X Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst))))
    (Iso.inv
        (α_ X Y (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)))) ≫
      tensorObj.{v, u} (𝒞 := inst) X Y ◁ hom (λ_ (tensorUnit.{v, u} C (𝒞 := inst))))
⊢ X ◁ hom (ρ_ Y) = Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y))

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]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.MonoidalCategory.associator_inv_naturality_right, CategoryTheory.MonoidalCategory.whiskerRight_iff, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.triangle_assoc_comp_right, CategoryTheory.MonoidalCategory.pentagon_inv_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.MonoidalCategory.associator_inv_naturality_middle