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

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

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

Tactic:
calc
      _ = 𝟙 _ ⊗≫ X ◁ η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 _ := by
        monoidal
      _ = 𝟙 _ ⊗≫ X ◁ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f := by
        rw [← whisker_exchange]; monoidal
      _ = f := by
        rw [evaluation_coevaluation'']; 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