-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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
⊢ 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 _)))
have 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 _)
Tactic: congr 3