-- 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
⊢ (f ≫ g)ᘁ =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Z _)))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
        (@rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁ η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
        (@rightDual.{v₁, u₁} _ inst inst_1 Z _ ◁ (g ⊗ₘ fᘁ) ≫
          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 simp : CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (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) (@rightDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (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) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
                (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
              (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 _)))
Tactic: simp only [rightAdjointMate, comp_whiskerRight]