-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
g : @rightDual.{v₁, u₁} _ inst inst_1 X _ ⟶ Z
rw :
  monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          ((tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y ◁ g ≫
              ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Z) ⊗≫
            𝟙 Z))) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
      (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
        @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ Y ◁ g) ≫
          Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y Z) ≫
            ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Z ≫ Iso.hom (λ_ Z))
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          ((ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
              tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ g) ⊗≫
            𝟙 Z))) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
      (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
        @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ (f ⊗ₘ g) ≫
          Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y Z) ≫
            ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Z ≫ Iso.hom (λ_ Z))

Tactic:
rw [← whisker_exchange, tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, CategoryTheory.MonoidalCategory.tensorHom_def