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 Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
⊢ (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))

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 Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
rw :
  monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y' ◁ η_ Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
⊢ monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))

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
X Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
⊢ monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y' ◁ η_ Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))

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 Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
rw :
  monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ Iso.hom ⊗𝟙 ) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    f
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    f

Tactic:
rw [coevaluation_evaluation'']

Premises used: CategoryTheory.ExactPairing.coevaluation_evaluation''
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ Iso.hom ⊗𝟙 ) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z 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
X Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
_ :
  (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
_₁ :
  monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
_₂ :
  monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    f
⊢ (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    f

Tactic:
calc
      _ = 𝟙 _ ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 _ := by
        monoidal
      _ = f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 _ := by
        rw [whisker_exchange]; monoidal
      _ = f := 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.ExactPairing.coevaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Y' Z Z' : C
inst_2 : ExactPairing Y Y'
f : tensorObj.{v₁, u₁} (𝒞 := inst) Y' X ⟶ Z
g : Z ⟶ Z'
⊢ Eq (α := X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y Z')
    ((tensorLeftHomEquiv X Y Y' Z' : (a : Y' ⊗ X ⟶ Z') → X ⟶ Y ⊗ Z') (f ≫ g) : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y Z')
    ((tensorLeftHomEquiv X Y Y' Z : (a : Y' ⊗ X ⟶ Z) → X ⟶ Y ⊗ Z) f ≫ Y ◁ g : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y Z')

Tactic:
simp [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
X X' Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' X ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv X Y Y' Z) : (a : X ⟶ Y ⊗ Z) → Y' ⊗ X ⟶ Z) (f ≫ g) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' X ⟶ Z)
    (Y' ◁ f ≫ (Equiv.symm (tensorLeftHomEquiv X' Y Y' Z) : (a : X' ⟶ Y ⊗ Z) → Y' ⊗ X' ⟶ Z) g :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' X ⟶ Z)

Tactic:
simp [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
X Y Y' Z Z' : C
inst_2 : ExactPairing Y Y'
f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z
g : Z ⟶ Z'
⊢ Eq (α := X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z' Y')
    ((tensorRightHomEquiv X Y Y' Z' : (a : X ⊗ Y ⟶ Z') → X ⟶ Z' ⊗ Y') (f ≫ g) :
      X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z' Y')
    ((tensorRightHomEquiv X Y Y' Z : (a : X ⊗ Y ⟶ Z) → X ⟶ Z ⊗ Y') f ≫ g ▷ Y' :
      X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z' Y')

Tactic:
simp [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
X X' Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z)
    ((Equiv.symm (tensorRightHomEquiv X Y Y' Z) : (a : X ⟶ Z ⊗ Y') → X ⊗ Y ⟶ Z) (f ≫ g) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z)
    (f ▷ Y ≫ (Equiv.symm (tensorRightHomEquiv X' Y Y' Z) : (a : X' ⟶ Z ⊗ Y') → X' ⊗ Y ⟶ Z) g :
      tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z)

Tactic:
simp [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
X X' Y Y' Z Z' : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Y Z
g : X' ⟶ Z'
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Z')
    ((Equiv.symm (tensorLeftHomEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) X X') Y Y' (tensorObj.{v₁, u₁} (𝒞 := inst) Z Z')) :
          (a : X ⊗ X' ⟶ Y ⊗ Z ⊗ Z') → Y' ⊗ X ⊗ X' ⟶ Z ⊗ Z')
        ((f ⊗ₘ g) ≫ Iso.hom (α_ Y Z Z')) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Z')
    (Iso.inv (α_ Y' X X') ≫ ((Equiv.symm (tensorLeftHomEquiv X Y Y' Z) : (a : X ⟶ Y ⊗ Z) → Y' ⊗ X ⟶ Z) f ⊗ₘ g) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Z')

Tactic:
simp [tensorLeftHomEquiv, tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.tensorLeftHomEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X X' Y Y' Z Z' : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
g : X' ⟶ Z'
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X' X) Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z' Z)
    ((Equiv.symm
            (tensorRightHomEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) X' X) Y Y' (tensorObj.{v₁, u₁} (𝒞 := inst) Z' Z)) :
          (a : X' ⊗ X ⟶ (Z' ⊗ Z) ⊗ Y') → (X' ⊗ X) ⊗ Y ⟶ Z' ⊗ Z)
        ((g ⊗ₘ f) ≫ Iso.inv (α_ Z' Z Y')) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X' X) Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z' Z)
    (Iso.hom (α_ X' X Y) ≫ (g ⊗ₘ (Equiv.symm (tensorRightHomEquiv X Y Y' Z) : (a : X ⟶ Z ⊗ Y') → X ⊗ Y ⟶ Z) f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X' X) Y ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z' Z)

Tactic:
simp [tensorRightHomEquiv, tensorHom_def]

Premises used: CategoryTheory.tensorRightHomEquiv, CategoryTheory.MonoidalCategory.tensorHom_def
-- 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) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (Y' ◁ (η_ Y Y' ≫ Y ◁ f) ≫ Iso.inv (α_ Y' Y Z) ≫ ε_ Y Y' ▷ Z ≫ Iso.hom (λ_ Z))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
        ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)

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 Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (Y' ◁ (η_ Y Y' ≫ Y ◁ f) ≫ Iso.inv (α_ Y' Y Z) ≫ ε_ Y Y' ▷ Z ≫ Iso.hom (λ_ Z))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ 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 Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((ε_ Y Y' ▷ Y' ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (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) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((ε_ Y Y' ▷ Y' ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (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) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y') (Iso.hom ⊗𝟙 ) f)
    (Iso.hom (ρ_ Y') ≫ f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
    (Iso.hom (ρ_ Y') ≫ f)

Tactic:
rw [coevaluation_evaluation'']

Premises used: CategoryTheory.ExactPairing.coevaluation_evaluation''
-- 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) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y') (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 Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
_ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
        ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
_₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
_₂ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
    (Iso.hom (ρ_ Y') ≫ f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (Iso.hom (ρ_ Y') ≫ f : tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)

Tactic:
calc
    _ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
      dsimp [tensorLeftHomEquiv]; monoidal
    _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
      rw [whisker_exchange]; monoidal
    _ = _ := 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.ExactPairing.coevaluation
-- 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 (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      @rightDual.{v₁, u₁} _ inst inst_1 X _)
    (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁
        (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫ 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.hom (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
      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 _))))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      @rightDual.{v₁, u₁} _ inst inst_1 X _)
    ((Equiv.symm
            (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
              (@rightDual.{v₁, u₁} _ inst inst_1 X _)) :
          (a : 𝟙_ C ⟶ Y ⊗ Xᘁ) → Yᘁ ⊗ 𝟙_ C ⟶ Xᘁ)
        (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
        @rightDual.{v₁, u₁} _ inst inst_1 X _)
    (Iso.hom (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ≫ fᘁ :
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
        @rightDual.{v₁, u₁} _ inst inst_1 X _)

Tactic:
dsimp [tensorLeftHomEquiv, rightAdjointMate]

Premises used: CategoryTheory.rightAdjointMate, 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 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      @rightDual.{v₁, u₁} _ inst inst_1 X _)
    (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁
        (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫ 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.hom (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
      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 _))))

Tactic:
simp