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

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc