awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
dsimp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
      @leftDual.{v₁, u₁} _ inst inst_1 X _)
    ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫ @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 _)))
    (Iso.hom (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 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 _))))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
      @leftDual.{v₁, u₁} _ inst inst_1 X _)
    ((Equiv.symm
            (tensorRightHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y
              (@leftDual.{v₁, u₁} _ inst inst_1 X _)) :
          (a : 𝟙_ C ⟶ ᘁX ⊗ Y) → 𝟙_ C ⊗ ᘁY ⟶ ᘁX)
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
        @leftDual.{v₁, u₁} _ inst inst_1 X _)
    (Iso.hom (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫ ᘁf :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
        @leftDual.{v₁, u₁} _ inst inst_1 X _)

Tactic:
dsimp [tensorRightHomEquiv, leftAdjointMate]

Premises used: CategoryTheory.leftAdjointMate, CategoryTheory.tensorRightHomEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
      @leftDual.{v₁, u₁} _ inst inst_1 X _)
    ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫ @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 _)))
    (Iso.hom (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 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 _))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
dsimp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    ((η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
      ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    ((Equiv.symm (tensorRightHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Z ⊗ Y') → 𝟙_ C ⊗ Y ⟶ Z)
        (η_ Y Y' ≫ f ▷ Y') :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
        ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)

Tactic:
dsimp [tensorRightHomEquiv]

Premises used: CategoryTheory.tensorRightHomEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    ((η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
      ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
      ((Y ◁ ε_ Y Y' ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
      ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') f)

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
      ((Y ◁ ε_ Y Y' ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') f)

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom ⊗𝟙 ) f)
    (Iso.hom (λ_ Y) ≫ f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') f)
    (Iso.hom (λ_ Y) ≫ f)

Tactic:
rw [evaluation_coevaluation'']

Premises used: CategoryTheory.ExactPairing.evaluation_coevaluation''
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom ⊗𝟙 ) f)
    (Iso.hom (λ_ Y) ≫ f)

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} Z
f : Y ⟶ @leftDual.{v₁, u₁} _ inst inst_1 Z _
dsimp :
  Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (λ_ Y) ≫
      η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ Y ≫
        Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z Y) ≫
          @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ (Z ◁ f ≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (𝟙 Y)
      ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ Y ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ◁ f) ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((tensorLeftHomEquiv Y (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)) :
          (a : Z ⊗ Y ⟶ 𝟙_ C) → Y ⟶ ᘁZ ⊗ 𝟙_ C)
        (Z ◁ f ≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z) :
      Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (𝟙 Y)
        ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ Y ≫
            tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ◁ f) ⊗≫
          @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z) :
      Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
dsimp [tensorLeftHomEquiv]

Premises used: CategoryTheory.tensorLeftHomEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} Z
f : Y ⟶ @leftDual.{v₁, u₁} _ inst inst_1 Z _
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (λ_ Y) ≫
      η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ Y ≫
        Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z Y) ≫
          @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ (Z ◁ f ≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (𝟙 Y)
      ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ Y ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ◁ f) ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} Z
f : Y ⟶ @leftDual.{v₁, u₁} _ inst inst_1 Z _
rw :
  Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (𝟙 Y)
      ((tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ≫
          η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _) ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) f
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (𝟙 Y)
      ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ Y ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ◁ f) ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) f
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} Z
f : Y ⟶ @leftDual.{v₁, u₁} _ inst inst_1 Z _
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (𝟙 Y)
      ((tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f ≫
          η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _) ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) f
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} Z
f : Y ⟶ @leftDual.{v₁, u₁} _ inst inst_1 Z _
rw :
  Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) f
      (Iso.hom ⊗𝟙 ))
    (f ≫ Iso.inv (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) f
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⊗≫
        @leftDual.{v₁, u₁} _ inst inst_1 Z _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z))
    (f ≫ Iso.inv (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))

Tactic:
rw [evaluation_coevaluation'']

Premises used: CategoryTheory.ExactPairing.evaluation_coevaluation''
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
Y Z : C
inst_2 : HasLeftDual.{v₁, u₁} Z
f : Y ⟶ @leftDual.{v₁, u₁} _ inst inst_1 Z _
⊢ Eq (α :=
    Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 Z _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) f
      (Iso.hom ⊗𝟙 ))
    (f ≫ Iso.inv (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
dsimp :
  Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 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 _ ≫
        Iso.hom (α_ (@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 _ ≫ ε_ (@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 _))) ≫
      Iso.inv (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)))
⊢ Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 Y _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((tensorLeftHomEquiv (@leftDual.{v₁, u₁} _ inst inst_1 Y _) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)) :
          (a : X ⊗ ᘁY ⟶ 𝟙_ C) → ᘁY ⟶ ᘁX ⊗ 𝟙_ C)
        (f ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y) :
      @leftDual.{v₁, u₁} _ inst inst_1 Y _ ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((ᘁf) ≫ Iso.inv (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)) :
      @leftDual.{v₁, u₁} _ inst inst_1 Y _ ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
dsimp [tensorLeftHomEquiv, leftAdjointMate]

Premises used: CategoryTheory.leftAdjointMate, CategoryTheory.tensorLeftHomEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
⊢ Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 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 _ ≫
        Iso.hom (α_ (@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 _ ≫ ε_ (@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 _))) ≫
      Iso.inv (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
dsimp :
  Eq (α :=
    @rightDual.{v₁, u₁} _ inst inst_1 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 _) ≫
        Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) ≫
          (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ≫ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ▷
            @rightDual.{v₁, u₁} _ inst inst_1 X _)
    (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 X _)))
⊢ Eq (α :=
    @rightDual.{v₁, u₁} _ inst inst_1 Y _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    ((tensorRightHomEquiv (@rightDual.{v₁, u₁} _ inst inst_1 Y _) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)) :
          (a : Yᘁ ⊗ X ⟶ 𝟙_ C) → Yᘁ ⟶ 𝟙_ C ⊗ Xᘁ)
        (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ≫ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) :
      @rightDual.{v₁, u₁} _ inst inst_1 Y _ ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (fᘁ ≫ Iso.inv (λ_ (@rightDual.{v₁, u₁} _ inst inst_1 X _)) :
      @rightDual.{v₁, u₁} _ inst inst_1 Y _ ⟶
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@rightDual.{v₁, u₁} _ inst inst_1 X _))

Tactic:
dsimp [tensorRightHomEquiv, rightAdjointMate]

Premises used: CategoryTheory.rightAdjointMate, CategoryTheory.tensorRightHomEquiv