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 : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
⊢ monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
have rw : monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
      (f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y' ◁ η_ Y Y')
      (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
  monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
    (monoidalComp (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
      (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
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) Z Y'
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    f
have rw : monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
    (monoidalComp (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
      (Z ◁ Iso.hom ⊗𝟙 ) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
  f
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' Z : C
inst_2 : ExactPairing Y Y'
f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'
⊢ (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    f
have _ : (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
    ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
      f) =
  monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
      (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
      (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
Tactic: calc
      _ = 𝟙 _ ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 _ := by
        monoidal
      _ = f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 _ := by
        rw [whisker_exchange]; monoidal
      _ = f := by
        rw [coevaluation_evaluation'']; monoidal
-- 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) Z Y'
_ :
  (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
⊢ (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    f
have _₁ : monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
      (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
      (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
  monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
    (monoidalComp (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
      (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
Tactic: calc
      _ = 𝟙 _ ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 _ := by
        monoidal
      _ = f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 _ := by
        rw [whisker_exchange]; monoidal
      _ = f := by
        rw [coevaluation_evaluation'']; monoidal
-- 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) Z Y'
_ :
  (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
_₁ :
  monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (𝟙 X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y'))
        (X ◁ η_ Y Y' ≫ f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')
        (Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
        (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y')))
⊢ (fun (f : tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ Z) ↦ Iso.inv (ρ_ X) ≫ X ◁ η_ Y Y' ≫ Iso.inv (α_ X Y Y') ≫ f ▷ Y')
      ((fun (f : X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z Y') ↦ f ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
        f) =
    f
have _₂ : monoidalComp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) f
    (monoidalComp (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y'))
      (Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y')) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z Y'))) =
  f
Tactic: calc
      _ = 𝟙 _ ⊗≫ (X ◁ η_ Y Y' ≫ f ▷ (Y ⊗ Y')) ⊗≫ Z ◁ ε_ Y Y' ▷ Y' ⊗≫ 𝟙 _ := by
        monoidal
      _ = f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 _ := by
        rw [whisker_exchange]; monoidal
      _ = f := by
        rw [coevaluation_evaluation'']; monoidal
-- 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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
        ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
have dsimp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  (Y' ◁ (η_ Y Y' ≫ Y ◁ f) ≫ Iso.inv (α_ Y' Y Z) ≫ ε_ Y Y' ▷ Z ≫ Iso.hom (λ_ Z))
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
    ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
Tactic: dsimp [tensorLeftHomEquiv]
-- 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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
    ((ε_ Y Y' ▷ Y' ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f) ⊗≫ 𝟙 Z))
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
    (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
    (Iso.hom (ρ_ Y') ≫ f)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y') (Iso.hom ⊗𝟙 ) f)
  (Iso.hom (ρ_ Y') ≫ f)
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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (Iso.hom (ρ_ Y') ≫ f : tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
have _ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
      (η_ Y Y' ≫ Y ◁ f) :
    tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z) :
    tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
Tactic: calc
    _ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
      dsimp [tensorLeftHomEquiv]; monoidal
    _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
      rw [whisker_exchange]; monoidal
    _ = _ := by rw [coevaluation_evaluation'']; monoidal
-- 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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
_ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
        ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (Iso.hom (ρ_ Y') ≫ f : tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
have _₁ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
    ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
    (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
Tactic: calc
    _ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
      dsimp [tensorLeftHomEquiv]; monoidal
    _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
      rw [whisker_exchange]; monoidal
    _ = _ := by rw [coevaluation_evaluation'']; monoidal
-- 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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y' ⟶ Z
_ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
        ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
_₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y) Y') (Y' ◁ η_ Y Y')
      ((tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
      (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    ((Equiv.symm (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Y ⊗ Z) → Y' ⊗ 𝟙_ C ⟶ Z)
        (η_ Y Y' ≫ Y ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
    (Iso.hom (ρ_ Y') ≫ f : tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
have _₂ : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) Y' (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ Z)
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y')
    (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') f)
  (Iso.hom (ρ_ Y') ≫ f)
Tactic: calc
    _ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
      dsimp [tensorLeftHomEquiv]; monoidal
    _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
      rw [whisker_exchange]; monoidal
    _ = _ := by rw [coevaluation_evaluation'']; monoidal
-- 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
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      @rightDual.{v₁, u₁} _ inst inst_1 X _)
    ((Equiv.symm
            (tensorLeftHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)
              (@rightDual.{v₁, u₁} _ inst inst_1 X _)) :
          (a : 𝟙_ C ⟶ Y ⊗ Xᘁ) → Yᘁ ⊗ 𝟙_ C ⟶ Xᘁ)
        (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
        @rightDual.{v₁, u₁} _ inst inst_1 X _)
    (Iso.hom (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ≫ fᘁ :
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
        @rightDual.{v₁, u₁} _ inst inst_1 X _)
have dsimp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    @rightDual.{v₁, u₁} _ inst inst_1 X _)
  (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
    Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _)) ≫
      ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
        Iso.hom (λ_ (@rightDual.{v₁, u₁} _ inst inst_1 X _)))
  (Iso.hom (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _)))
      (@rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
        @rightDual.{v₁, u₁} _ inst inst_1 Y _ ◁ f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
          Iso.inv (α_ (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _)) ≫
            ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫
              Iso.hom (λ_ (@rightDual.{v₁, u₁} _ inst inst_1 X _))))
Tactic: dsimp [tensorLeftHomEquiv, rightAdjointMate]
-- 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
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
      @leftDual.{v₁, u₁} _ inst inst_1 X _)
    ((Equiv.symm
            (tensorRightHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y
              (@leftDual.{v₁, u₁} _ inst inst_1 X _)) :
          (a : 𝟙_ C ⟶ ᘁX ⊗ Y) → 𝟙_ C ⊗ ᘁY ⟶ ᘁX)
        (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
        @leftDual.{v₁, u₁} _ inst inst_1 X _)
    (Iso.hom (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫ ᘁf :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
        @leftDual.{v₁, u₁} _ inst inst_1 X _)
have dsimp : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _) ⟶
    @leftDual.{v₁, u₁} _ inst inst_1 X _)
  ((η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) ▷
      @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
    Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
      @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
        Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)))
  (Iso.hom (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Y _))
      (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _)))
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Y _ ≫
          Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Y (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) ≫
            @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ≫
              Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _))))
Tactic: dsimp [tensorRightHomEquiv, leftAdjointMate]
-- 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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    ((Equiv.symm (tensorRightHomEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y Y' Z) : (a : 𝟙_ C ⟶ Z ⊗ Y') → 𝟙_ C ⊗ Y ⟶ Z)
        (η_ Y Y' ≫ f ▷ Y') :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
        ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
have dsimp : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
  ((η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ Iso.hom (α_ Z Y' Y) ≫ Z ◁ ε_ Y Y' ≫ Iso.hom (ρ_ Z))
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
    ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z))
Tactic: dsimp [tensorRightHomEquiv]
-- 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
Y Y' Z : C
inst_2 : ExactPairing Y Y'
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
      ((f ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z))
    (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') f)
have rw : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Z)
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorObj.{v₁, u₁} (𝒞 := inst) Y' Y)) (η_ Y Y' ▷ Y)
    ((Y ◁ ε_ Y Y' ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⊗≫ 𝟙 Z))
  (monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y')
    f)
Tactic: rw [← whisker_exchange]