-- 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 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
g : @leftDual.{v₁, u₁} _ inst inst_1 X _ ⟶ Z
rw :
  monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
          ((g ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ≫
              Z ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y) ⊗≫
            𝟙 Z))) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ g ▷ Y) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
          Iso.hom (α_ Z Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
            Z ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫ Iso.hom (ρ_ Z))
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _)
          ((@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
              g ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫
            𝟙 Z))) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
        (g ⊗ₘ f) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
          Iso.hom (α_ Z Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
            Z ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫ Iso.hom (ρ_ Z))

Tactic:
rw [whisker_exchange, tensorHom_def']

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