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 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) =
    f
have _ : (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))
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
-- 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' 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))
⊢ (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
have _₁ : 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: 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
-- 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' 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)
⊢ (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
have _₂ : 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: 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
-- 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' 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))
        (η_ 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)))
have 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)))
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' 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)
        ((η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ▷ Z) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) =
    f
have 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
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' 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) =
    f
have _ : (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: 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
-- 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' 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)))
⊢ (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
have _₁ : 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: 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
-- 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' 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)))
⊢ (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
have _₂ : 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: 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
-- 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' 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) ((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)
have 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)
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' 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 ◁ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y')) f) =
    f
have 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
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' 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) =
    f
have _ : (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: 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
-- 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' 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))
⊢ (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
have _₁ : 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: 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
-- 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' 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)
⊢ (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
have _₂ : 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: 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