awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
    ((((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X))) ≫
      inv (Y ◁ Iso.inv (β_ Y X)))
    ((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
          Iso.inv (α_ X Y Y)) ≫
        Iso.hom (β_ X Y) ▷ Y) ≫
      Iso.hom (α_ Y X Y))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X)))
    (((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
            Iso.inv (α_ X Y Y)) ≫
          Iso.hom (β_ X Y) ▷ Y) ≫
        Iso.hom (α_ Y X Y)) ≫
      Y ◁ Iso.inv (β_ Y X))

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
    ((((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X))) ≫
      inv (Y ◁ Iso.inv (β_ Y X)))
    ((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
          Iso.inv (α_ X Y Y)) ≫
        Iso.hom (β_ X Y) ▷ Y) ≫
      Iso.hom (α_ Y X Y))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                  Iso.inv (α_ X Y Y)) ≫
                Iso.hom (β_ X Y) ▷ Y) ≫
              Iso.hom (α_ Y X Y)) ≫
            Y ◁ Iso.inv (β_ Y X)) ≫
          Iso.inv (α_ Y Y X)) ≫
        Iso.inv (β_ Y Y) ▷ X) ≫
      Iso.hom (α_ Y Y X))

Tactic:
iterate 4 rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
    ((((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X))) ≫
      inv (Y ◁ Iso.inv (β_ Y X)))
    ((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
          Iso.inv (α_ X Y Y)) ≫
        Iso.hom (β_ X Y) ▷ Y) ≫
      Iso.hom (α_ Y X Y))

Tactic:
simpa using (yang_baxter Y X Y).symm

Premises used: CategoryTheory.BraidedCategory.yang_baxter, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (η_ X Y ▷ Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y))
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y)
              (X ◁ Iso.hom (β_ Y Y))
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
                (Iso.hom (β_ X Y) ▷ Y)
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
                  (Y ◁ Iso.inv (β_ Y X))
                  (Iso.inv (β_ Y Y) ▷ X ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)))))))
          (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)) =
    monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y)
        (η_ X Y ▷ Y ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
        ((Iso.inv (β_ Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)) ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y))

Tactic:
simp [monoidalComp, braiding_tensor_left_hom, braiding_tensor_right_inv]

Premises used: CategoryTheory.monoidalComp, CategoryTheory.BraidedCategory.braiding_tensor_left_hom, CategoryTheory.BraidedCategory.braiding_tensor_right_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
rw :
  monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y)
        (Iso.hom (β_ (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) ≫ Y ◁ η_ X Y)
        ((ε_ X Y ▷ Y ≫ Iso.inv (β_ Y (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))) ⊗≫ 𝟙 Y)) =
    𝟙 Y
⊢ monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y)
        (η_ X Y ▷ Y ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
        ((Iso.inv (β_ Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)) ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y)) =
    𝟙 Y

Tactic:
rw [braiding_naturality_left, ← braiding_inv_naturality_left]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_left, CategoryTheory.BraidedCategory.braiding_inv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y)
        (Iso.hom (β_ (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) ≫ Y ◁ η_ X Y)
        ((ε_ X Y ▷ Y ≫ Iso.inv (β_ Y (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))) ⊗≫ 𝟙 Y)) =
    𝟙 Y

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : LeftRigidCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    { unmop := op (@HasLeftDual.leftDual.{v, u} _ inst inst_1 X _) : Cᵒᵖᴹᵒᵖ } ⟶
      { unmop := op (@HasLeftDual.leftDual.{v, u} _ inst inst_1 X _) })
    (Quiver.Hom.mop (Quiver.Hom.op (ᘁ𝟙 X))) (𝟙 { unmop := op (@HasLeftDual.leftDual.{v, u} _ inst inst_1 X _) })

Tactic:
simp [leftAdjointMate_id]

Premises used: CategoryTheory.leftAdjointMate_id
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : LeftRigidCategory.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v + 1} (α :=
    { unmop := op (@HasLeftDual.leftDual.{v, u} _ inst inst_1 X _) : Cᵒᵖᴹᵒᵖ } ⟶
      { unmop := op (@HasLeftDual.leftDual.{v, u} _ inst inst_1 Z _) })
    (Quiver.Hom.mop (Quiver.Hom.op (ᘁf ≫ g)))
    (CategoryStruct.comp (Y := { unmop := op (@HasLeftDual.leftDual.{v, u} _ inst inst_1 Y _) })
      (Quiver.Hom.mop (Quiver.Hom.op (ᘁf))) (Quiver.Hom.mop (Quiver.Hom.op (ᘁg))))

Tactic:
simp [comp_leftAdjointMate]

Premises used: CategoryTheory.comp_leftAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : RightRigidCategory.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    { unmop := op (@HasRightDual.rightDual.{v, u} _ inst inst_1 X _) : Cᵒᵖᴹᵒᵖ } ⟶
      { unmop := op (@HasRightDual.rightDual.{v, u} _ inst inst_1 X _) })
    (Quiver.Hom.mop (Quiver.Hom.op (𝟙 Xᘁ))) (𝟙 { unmop := op (@HasRightDual.rightDual.{v, u} _ inst inst_1 X _) })

Tactic:
simp [rightAdjointMate_id]

Premises used: CategoryTheory.rightAdjointMate_id
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Functor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : RightRigidCategory.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v + 1} (α :=
    { unmop := op (@HasRightDual.rightDual.{v, u} _ inst inst_1 X _) : Cᵒᵖᴹᵒᵖ } ⟶
      { unmop := op (@HasRightDual.rightDual.{v, u} _ inst inst_1 Z _) })
    (Quiver.Hom.mop (Quiver.Hom.op ((f ≫ g)ᘁ)))
    (CategoryStruct.comp (Y := { unmop := op (@HasRightDual.rightDual.{v, u} _ inst inst_1 Y _) })
      (Quiver.Hom.mop (Quiver.Hom.op (fᘁ))) (Quiver.Hom.mop (Quiver.Hom.op (gᘁ))))

Tactic:
simp [comp_rightAdjointMate]

Premises used: CategoryTheory.comp_rightAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ⟶
      @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Z) _)
    (F.map (inv (f ≫ g))ᘁ)
    (CategoryStruct.comp (Y := @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.map (inv f)ᘁ)
      (F.map (inv g)ᘁ))

Tactic:
simp [comp_rightAdjointMate]

Premises used: CategoryTheory.comp_rightAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ F.map (inv f)ᘁ))
⊢ Functor.map ((𝟙_ (Functor.{u_3, v_1, u_1, u_2} C D)) (𝒞 := Functor.category)) f ≫
      η_ (F.obj Y)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }
          Y) =
    η_ (F.obj X)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          X) ≫
      (tensorObj (𝒞 := Functor.category) F
            { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
              map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
              Functor.{u_3, v_1, u_1, u_2} C D }).map
        f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ≫
      𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)))
⊢ (tensorObj (𝒞 := Functor.category)
            { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
              map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
              Functor.{u_3, v_1, u_1, u_2} C D }
            F).map
        f ≫
      ε_ (F.obj Y)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          Y) =
    ε_ (F.obj X)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          X) ≫
      Functor.map ((𝟙_ (Functor.{u_3, v_1, u_1, u_2} C D)) (𝒞 := Functor.category)) f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : LeftRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _ ⟶
      @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Z) _)
    (ᘁF.map (inv (f ≫ g)))
    (CategoryStruct.comp (Y := @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (ᘁF.map (inv f))
      (ᘁF.map (inv g)))

Tactic:
simp [comp_leftAdjointMate]

Premises used: CategoryTheory.comp_leftAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : LeftRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
⊢ Functor.map ((𝟙_ (Functor.{u_3, v_1, u_1, u_2} C D)) (𝒞 := Functor.category)) f ≫
      η_
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }
          Y)
        (F.obj Y) =
    η_
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          X)
        (F.obj X) ≫
      (tensorObj (𝒞 := Functor.category)
            { obj := fun (X : C) ↦ @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
              map := fun {X Y : C} (f : X ⟶ Y) ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ :
              Functor.{u_3, v_1, u_1, u_2} C D }
            F).map
        f

Tactic:
simp [tensorHom_def, coevaluation_comp_leftAdjointMate_assoc]

Premises used: CategoryTheory.coevaluation_comp_leftAdjointMate_assoc, CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : LeftRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
⊢ (tensorObj (𝒞 := Functor.category) F
            { obj := fun (X : C) ↦ @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
              map := fun {X Y : C} (f : X ⟶ Y) ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ :
              Functor.{u_3, v_1, u_1, u_2} C D }).map
        f ≫
      ε_
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          Y)
        (F.obj Y) =
    ε_
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasLeftDual.leftDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          X)
        (F.obj X) ≫
      Functor.map ((𝟙_ (Functor.{u_3, v_1, u_1, u_2} C D)) (𝒞 := Functor.category)) f

Tactic:
simp [tensorHom_def, leftAdjointMate_comp_evaluation]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.leftAdjointMate_comp_evaluation
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
inst_5 : F.Faithful
X Y : C
eval : tensorObj.{v_1, u_1} (𝒞 := inst) Y X ⟶ tensorUnit.{v_1, u_1} C (𝒞 := inst)
coeval : tensorUnit.{v_1, u_1} C (𝒞 := inst) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X Y
inst_6 : ExactPairing (F.obj X) (F.obj Y)
map_eval :
  F.map eval =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj Y) (F.obj X)) (δ F Y X)
      (ε_ (F.obj X) (F.obj Y) ≫ ε F)
map_coeval :
  F.map coeval =
    CategoryStruct.comp (Y := tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (η F) (η_ (F.obj X) (F.obj Y) ≫ μ F X Y)
⊢ F.map (Y ◁ coeval ≫ Iso.inv (α_ Y X Y) ≫ eval ▷ Y) = F.map (Iso.hom (ρ_ Y) ≫ Iso.inv (λ_ Y))

Tactic:
simp [map_eval, map_coeval, Functor.Monoidal.map_whiskerLeft,
        Functor.Monoidal.map_whiskerRight]

Premises used: CategoryTheory.Functor.Monoidal.map_whiskerRight, CategoryTheory.Functor.Monoidal.map_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
inst_5 : F.Faithful
X Y : C
eval : tensorObj.{v_1, u_1} (𝒞 := inst) Y X ⟶ tensorUnit.{v_1, u_1} C (𝒞 := inst)
coeval : tensorUnit.{v_1, u_1} C (𝒞 := inst) ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) X Y
inst_6 : ExactPairing (F.obj X) (F.obj Y)
map_eval :
  F.map eval =
    CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj Y) (F.obj X)) (δ F Y X)
      (ε_ (F.obj X) (F.obj Y) ≫ ε F)
map_coeval :
  F.map coeval =
    CategoryStruct.comp (Y := tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (η F) (η_ (F.obj X) (F.obj Y) ≫ μ F X Y)
⊢ F.map (coeval ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ eval) = F.map (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
simp [map_eval, map_coeval, Functor.Monoidal.map_whiskerLeft,
        Functor.Monoidal.map_whiskerRight]

Premises used: CategoryTheory.Functor.Monoidal.map_whiskerRight, CategoryTheory.Functor.Monoidal.map_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
X Y : C
inst_7 : ExactPairing (F.obj X) (F.obj Y)
⊢ Eq (α := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y X) ⟶ F.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (F.map
      (F.preimage
        (CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj Y) (F.obj X)) (δ F Y X)
          (ε_ (F.obj X) (F.obj Y) ≫ ε F))))
    (CategoryStruct.comp (Y := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj Y) (F.obj X)) (δ F Y X)
      (ε_ (F.obj X) (F.obj Y) ≫ ε F))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
X Y : C
inst_7 : ExactPairing (F.obj X) (F.obj Y)
⊢ Eq (α := F.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
    (F.map
      (F.preimage
        (CategoryStruct.comp (Y := tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (η F) (η_ (F.obj X) (F.obj Y) ≫ μ F X Y))))
    (CategoryStruct.comp (Y := tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (η F) (η_ (F.obj X) (F.obj Y) ≫ μ F X Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_5 : F.IsEquivalence
X : C
inst_6 : HasLeftDual.{v_2, u_2} (F.obj X)
this : ExactPairing (F.obj (G.obj (@HasLeftDual.leftDual.{v_2, u_2} _ inst_1 inst_3 (F.obj X) _))) (F.obj X) :=
  exactPairingCongrLeft (adj.toEquivalence.counitIso.app (@HasLeftDual.leftDual.{v_2, u_2} _ inst_1 inst_3 (F.obj X) _))
⊢ ExactPairing (G.obj (@HasLeftDual.leftDual.{v_2, u_2} _ inst_1 inst_3 (F.obj X) _)) X

Tactic:
apply ExactPairing.ofFullyFaithful F

Premises used: CategoryTheory.ExactPairing.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_5 : F.IsEquivalence
X : C
inst_6 : HasRightDual.{v_2, u_2} (F.obj X)
this : ExactPairing (F.obj X) (F.obj (G.obj (@HasRightDual.rightDual.{v_2, u_2} _ inst_1 inst_3 (F.obj X) _))) :=
  exactPairingCongrRight
    (adj.toEquivalence.counitIso.app (@HasRightDual.rightDual.{v_2, u_2} _ inst_1 inst_3 (F.obj X) _))
⊢ ExactPairing X (G.obj (@HasRightDual.rightDual.{v_2, u_2} _ inst_1 inst_3 (F.obj X) _))

Tactic:
apply ExactPairing.ofFullyFaithful F

Premises used: CategoryTheory.ExactPairing.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ) ↔
    ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro