-- 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) (@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 _)
⊢ 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 _)))

Tactic:
congr 3