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 Z : C
inst_2 : HasRightDual.{v₁, u₁} X
inst_3 : HasRightDual.{v₁, u₁} Y
inst_4 : HasRightDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (monoidalComp (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
            (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
          (monoidalComp (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _))
                Y)
              (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) Y
                (tensorObj.{v₁, u₁} (𝒞 := inst) (@rightDual.{v₁, u₁} _ inst inst_1 Y _) Y))
              (η_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _) ▷ Y) (Y ◁ ε_ Y (@rightDual.{v₁, u₁} _ inst inst_1 Y _)) ▷
            @rightDual.{v₁, u₁} _ inst inst_1 X _)
          (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
            𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))) =
    η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
      f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _
have rw : monoidalComp (X := tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _))
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y)
        (@rightDual.{v₁, u₁} _ inst inst_1 X _))
      (f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Y (@rightDual.{v₁, u₁} _ inst inst_1 X _))
        (Iso.hom ⊗𝟙 ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _)
        (g ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ⊗≫
          𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Z (@rightDual.{v₁, u₁} _ inst inst_1 X _))))) =
  η_ X (@rightDual.{v₁, u₁} _ inst inst_1 X _) ≫
    f ▷ @rightDual.{v₁, u₁} _ inst inst_1 X _ ≫ g ▷ @rightDual.{v₁, u₁} _ inst inst_1 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶ @leftDual.{v₁, u₁} _ inst inst_1 X _) (ᘁf ≫ g)
    (CategoryStruct.comp (Y := @leftDual.{v₁, u₁} _ inst inst_1 Y _) (ᘁg) (ᘁf))
have rw : (ᘁf ≫ g) =
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
      ((ᘁf) ⊗ₘ g) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
        Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
          @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ≫
            Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)))
Tactic: rw [leftAdjointMate_comp]
-- 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ᘁf ≫ g) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
      (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
        ((ᘁf) ⊗ₘ g) ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
          Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
            @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ≫
              Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)))
have simp : CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
      (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g) ▷
          @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
        Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
          @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ≫
            Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _))) =
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)))
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
      (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 _))) ⊗ₘ
            g) ▷
          @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
        Iso.hom (α_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
          @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _) Z ≫
            Iso.hom (ρ_ (@leftDual.{v₁, u₁} _ inst inst_1 X _)))
Tactic: simp only [leftAdjointMate, MonoidalCategory.whiskerLeft_comp]
-- 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
        (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
    ((Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
        η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _) ≫
      (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g) ▷
        @leftDual.{v₁, u₁} _ inst inst_1 Z _)
    ((Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
        η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _) ≫
      (CategoryStruct.comp (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 _) ≫
                  (@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 _))) ⊗ₘ
          g) ▷
        @leftDual.{v₁, u₁} _ inst inst_1 Z _)
have e_a : Eq (α :=
  @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
      (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
  (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
    η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
      (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g) ▷
        @leftDual.{v₁, u₁} _ inst inst_1 Z _)
  (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
    η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
      (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 _))) ⊗ₘ
          g) ▷
        @leftDual.{v₁, u₁} _ inst inst_1 Z _)
Tactic: simp only [Category.assoc]
-- 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
        (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g) ▷
          @leftDual.{v₁, u₁} _ inst inst_1 Z _)
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ @leftDual.{v₁, u₁} _ inst inst_1 Z _ ≫
        (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 _))) ⊗ₘ
            g) ▷
          @leftDual.{v₁, u₁} _ inst inst_1 Z _)
have e_a : Eq (α :=
  @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
      (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
  (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
        @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g) ▷
      @leftDual.{v₁, u₁} _ inst inst_1 Z _)
  (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
    (η_ (@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 _))) ⊗ₘ
          g)) ▷
      @leftDual.{v₁, u₁} _ inst inst_1 Z _)
Tactic: simp only [← comp_whiskerRight]
-- 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @leftDual.{v₁, u₁} _ inst inst_1 Z _ ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
        (@leftDual.{v₁, u₁} _ inst inst_1 Z _))
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
          @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g) ▷
        @leftDual.{v₁, u₁} _ inst inst_1 Z _)
    (Iso.inv (λ_ (@leftDual.{v₁, u₁} _ inst inst_1 Z _)) ≫
      (η_ (@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 _))) ⊗ₘ
            g)) ▷
        @leftDual.{v₁, u₁} _ inst inst_1 Z _)
have e_a : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
  (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
    @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)
  (η_ (@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 _))) ⊗ₘ
      g))
Tactic: congr 2
-- 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
      @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)
    (η_ (@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 _))) ⊗ₘ
        g))
have e_a : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
  (η_ (@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 _))) ⊗ₘ
      g))
  (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
    @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)
Tactic: 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 Z : C
inst_2 : HasLeftDual.{v₁, u₁} X
inst_3 : HasLeftDual.{v₁, u₁} Y
inst_4 : HasLeftDual.{v₁, u₁} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
    (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
      (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f)
        (monoidalComp (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁
            (Y ◁ η_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ⊗≫ ε_ (@leftDual.{v₁, u₁} _ inst inst_1 Y _) Y ▷ Y))
          (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g))))
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
      @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)
have rw : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) Z)
  (monoidalComp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
    (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X)
    (monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f)
      (monoidalComp (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@leftDual.{v₁, u₁} _ inst inst_1 X _)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y))
        (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ Iso.hom ⊗𝟙 ) (@leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g))))
  (η_ (@leftDual.{v₁, u₁} _ inst inst_1 X _) X ≫
    @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ f ≫ @leftDual.{v₁, u₁} _ inst inst_1 X _ ◁ g)
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 : tensorObj.{v₁, u₁} (𝒞 := inst) Y' X ⟶ 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)
have rw : 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)
      ((ε_ Y Y' ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y' X ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f) ⊗≫ 𝟙 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: 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) Y' X ⟶ 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) =
    f
have rw : 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)
      (Iso.hom ⊗𝟙 ▷ X) f) =
  f
Tactic: rw [coevaluation_evaluation'']