-- 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
e_a :
  Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
        (@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.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 _)
⊢ Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
        (@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.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 _)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc