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