awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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 ≫ i.inv ▷ Y) ≫ Iso.inv (α_ Y X Y) ≫ (Y ◁ i.hom ≫ ε_ X' Y) ▷ Y) (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))
have _₁ : 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)
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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 (α :=
    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))
have _₂ : 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: 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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)
      ((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)))))
have 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)))))
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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'))
        (η_ 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)))))
have 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)))))
Tactic: rw [← whisker_exchange, ← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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)))
          (η_ 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)))
have 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)))
Tactic: rw [evaluation_coevaluation'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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) ⊗≫
      (i.hom ≫ i.inv) ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X)
have 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)
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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')
      ((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)))
have 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)))
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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')
        (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)))
have 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)))
Tactic: rw [whisker_exchange, whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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')
          (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)
have 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)
Tactic: rw [coevaluation_evaluation'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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))) ⊗≫
      (i.hom ≫ i.inv) ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) =
    Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y)
have 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)
Tactic: rw [Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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 ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y') (η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y')
have 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')
Tactic: rw [Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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 ◁ ε_ X Y') (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
have rw : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.hom ⊗𝟙 ) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
Tactic: rw [evaluation_coevaluation'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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')) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
have _ : 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: calc
      _ = η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y' := by
        monoidal
      _ = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y' := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [evaluation_coevaluation'']
        simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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')
⊢ 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')) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
have _₁ : 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: calc
      _ = η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y' := by
        monoidal
      _ = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y' := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [evaluation_coevaluation'']
        simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
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')
_₁ :
  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')
⊢ 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')) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
have _₂ : 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 ◁ ε_ X Y') (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
Tactic: calc
      _ = η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y' := by
        monoidal
      _ = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y' := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [evaluation_coevaluation'']
        simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ Eq.{v₁ + 1} (α := Y₁ ⟶ Y₁) (CategoryStruct.comp (Y := Y₂) (𝟙 Xᘁ) (𝟙 Xᘁ) : Y₁ ⟶ Y₁) (𝟙 Y₁ : Y₁ ⟶ Y₁)
have rw : Eq.{v₁ + 1} (α := Y₁ ⟶ Y₁) (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (𝟙 Y₁)
Tactic: rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ Eq.{v₁ + 1} (α := Y₂ ⟶ Y₂) (CategoryStruct.comp (Y := Y₁) (𝟙 Xᘁ) (𝟙 Xᘁ) : Y₂ ⟶ Y₂) (𝟙 Y₂ : Y₂ ⟶ Y₂)
have rw : Eq.{v₁ + 1} (α := Y₂ ⟶ Y₂) (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (𝟙 Y₂)
Tactic: rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ Eq.{v₁ + 1} (α := X₁ ⟶ X₁) (CategoryStruct.comp (Y := X₂) (ᘁ𝟙 Y) (ᘁ𝟙 Y) : X₁ ⟶ X₁) (𝟙 X₁ : X₁ ⟶ X₁)
have rw : Eq.{v₁ + 1} (α := X₁ ⟶ X₁) (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) (𝟙 X₁)
Tactic: rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ Eq.{v₁ + 1} (α := X₂ ⟶ X₂) (CategoryStruct.comp (Y := X₁) (ᘁ𝟙 Y) (ᘁ𝟙 Y) : X₂ ⟶ X₂) (𝟙 X₂ : X₂ ⟶ X₂)
have rw : Eq.{v₁ + 1} (α := X₂ ⟶ X₂) (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) (𝟙 X₂)
Tactic: rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
p : ExactPairing X Y
⊢ rightDualIso p p = Iso.refl Y
have w : (rightDualIso p p).hom = Iso.hom (Iso.refl Y)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
p : ExactPairing X Y
⊢ leftDualIso p p = Iso.refl X
have w : (leftDualIso p p).hom = Iso.hom (Iso.refl X)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) X)
    (X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X)
    (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X))
have rw : Eq.{v_1 + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
    (Iso.inv (ρ_ X))
    ((X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X) ≫ Iso.hom (λ_ X)))
  (𝟙 X)
Tactic: rw [Iso.eq_comp_inv, ← Iso.inv_comp_eq_id]