-- 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 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
_ :
  η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
      (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 _)))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Y
          (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))))
        (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ◁
            η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) Y
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
              (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
          (Y ◁ @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
            (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
            (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
              𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
_₁ :
  monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
          (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Y
          (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))))
        (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ◁
            η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (monoidalComp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) Y
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
              (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
          (Y ◁ @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
            (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
            (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
              𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _)))))) =
    monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Y
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷
            tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ◁
            f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _)))))
_₂ :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
        (tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Y
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y)
            (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
        (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷
            tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ◁
            f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (monoidalComp (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
                Y)
              (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) Y
                (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y))
              (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Y) (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ▷
            @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))))
_₃ :
  monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (monoidalComp (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
                Y)
              (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) Y
                (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y))
              (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Y) (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ▷
            @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))) =
    η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
      f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ≫
      (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 _)))))
    (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
      f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)

Tactic:
calc
    _ = 𝟙 _ ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫
        Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 _ := by
      rw [tensorHom_def']; monoidal
    _ = η_ X Xᘁ ⊗≫ (η_ Y Yᘁ ▷ (X ⊗ Xᘁ) ≫ (Y ⊗ Yᘁ) ◁ f ▷ Xᘁ) ⊗≫
        Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; monoidal
    _ = η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; monoidal
    _ = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ := by
      rw [evaluation_coevaluation'']; monoidal

Premises used: CategoryTheory.HasRightDual.rightDual, CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.monoidalComp, CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.ExactPairing.evaluation, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.CategoryStruct.comp, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.ExactPairing.coevaluation