-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : HasRightDual.{v₁, u₁} X
f : Y ⟶ @rightDual.{v₁, u₁} _ inst inst_1 X _
rw :
  Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 Y)
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _) X)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          @rightDual.{v₁, u₁} _ inst inst_1 X _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (ε_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _) X)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (@rightDual.{v₁, u₁} _ inst inst_1 X _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (ε_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)))
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 Y)
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _) X)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (Y ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (ε_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 X _) X)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (@rightDual.{v₁, u₁} _ inst inst_1 X _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (ε_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)))

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange