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

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

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