-- 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) (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 _)))
have 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 _)))
Tactic: simp only [← Category.assoc]