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

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 X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Iso.hom ⊗𝟙 ) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
_ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ (η_ X' Y ≫ i.inv ▷ Y) ≫ Iso.inv (α_ Y X Y) ≫ (Y ◁ i.hom ≫ ε_ X' Y) ▷ Y)
    (Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y)
_₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y) (Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y)
_₂ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
    (Y ◁ (η_ X' Y ≫ i.inv ▷ Y) ≫ Iso.inv (α_ Y X Y) ≫ (Y ◁ i.hom ≫ ε_ X' Y) ▷ Y) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))

Tactic:
calc
      _ = Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y := by
        monoidal
      _ = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [coevaluation_evaluation'']
        simp

Premises used: CategoryTheory.ExactPairing.evaluation, CategoryTheory.CategoryStruct.comp, CategoryTheory.ExactPairing.coevaluation, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((η_ X' Y ≫ i.inv ▷ Y) ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ (Y ◁ i.hom ≫ ε_ X' Y))
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (η_ X' Y ▷ X)
      ((i.inv ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y X ≫ X ◁ Y ◁ i.hom) ⊗≫ X ◁ ε_ X' 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 X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
rw :
  monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (η_ X' Y ▷ X)
      ((X' ◁ Y ◁ i.hom ≫ i.inv ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y X') ⊗≫ X ◁ ε_ X' Y) =
    monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
      (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorObj.{v₁, u₁} (𝒞 := inst) Y X'))
        (η_ X' Y ▷ X ≫ tensorObj.{v₁, u₁} (𝒞 := inst) X' Y ◁ i.hom)
        ((i.inv ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y X' ≫ X ◁ ε_ X' Y) ⊗≫
          𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
⊢ monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)) (η_ X' Y ▷ X)
      ((i.inv ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y X ≫ X ◁ Y ◁ i.hom) ⊗≫ X ◁ ε_ X' Y) =
    monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
      (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorObj.{v₁, u₁} (𝒞 := inst) Y X'))
        (η_ X' Y ▷ X ≫ tensorObj.{v₁, u₁} (𝒞 := inst) X' Y ◁ i.hom)
        ((i.inv ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y X' ≫ X ◁ ε_ X' Y) ⊗≫
          𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))

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

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

Tactic:
rw [← whisker_exchange, ← 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 X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
⊢ monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)
      (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
      (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorObj.{v₁, u₁} (𝒞 := inst) Y X'))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ i.hom ≫ η_ X' Y ▷ X')
        ((X' ◁ ε_ X' Y ≫ i.inv ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫
          𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⊗≫
      monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X') i.hom
        (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (η_ X' Y ▷ X' ⊗≫ X' ◁ ε_ X' Y)
          (i.inv ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))

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

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 X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⊗≫
      monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X') i.hom
        (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X' (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.hom ⊗𝟙 )
          (i.inv ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⊗≫
      (i.hom ≫ i.inv) ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
rw :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⊗≫
      𝟙 X ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⊗≫
      (i.hom ≫ i.inv) ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X X' Y : C
inst_2 : ExactPairing X' Y
i : X ≅ X'
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⊗≫
      𝟙 X ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)

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

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

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' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗≫
      monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst))) i.hom
        (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y') (Iso.hom ⊗𝟙 )
          (i.inv ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y))) =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗≫
      (i.hom ≫ i.inv) ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
rw :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗≫
      𝟙 Y ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) =
    Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y)
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗≫
      (i.hom ≫ i.inv) ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) =
    Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y)

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Y' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗≫
      𝟙 Y ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) =
    Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ 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' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((η_ X Y' ≫ X ◁ i.inv) ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ (i.hom ▷ X ≫ ε_ X Y'))
    (η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X 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' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y' ▷ X ⊗≫ X ◁ 𝟙 Y' ▷ X ≫ X ◁ ε_ X Y') (η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y')
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y') (η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y')

Tactic:
rw [Iso.inv_hom_id]

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

Tactic:
monoidal