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