awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
e : Y ≅ X
x : F.CorepresentableBy X
h :
  Eq.{w + 1} (α := F.obj X)
    ((homEquiv
            ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm)
              ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) x)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
    (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)
⊢ (fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) x) = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
e : Y ≅ X
x : F.CorepresentableBy X
⊢ Eq.{w + 1} (α := F.obj X)
    ((homEquiv
            ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm)
              ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) x)) :
          (a : X ⟶ X) → F.obj X)
        (𝟙 X) :
      F.obj X)
    (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (X ⟶ X) (F.obj X)) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
e : Y ≅ X
x : F.CorepresentableBy Y
h :
  Eq.{w + 1} (α := F.obj Y)
    ((homEquiv
            ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e)
              ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) x)) :
          (a : Y ⟶ Y) → F.obj Y)
        (𝟙 Y) :
      F.obj Y)
    (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (Y ⟶ Y) (F.obj Y)) : (a : Y ⟶ Y) → F.obj Y) (𝟙 Y) : F.obj Y)
⊢ (fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e) ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) x) = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X Y : C
e : Y ≅ X
x : F.CorepresentableBy Y
⊢ Eq.{w + 1} (α := F.obj Y)
    ((homEquiv
            ((fun (R : F.CorepresentableBy X) ↦ R.ofIsoObj e)
              ((fun (R : F.CorepresentableBy Y) ↦ R.ofIsoObj e.symm) x)) :
          (a : Y ⟶ Y) → F.obj Y)
        (𝟙 Y) :
      F.obj Y)
    (((x.homEquiv : Equiv.{v₁ + 1, w + 1} (Y ⟶ Y) (F.obj Y)) : (a : Y ⟶ Y) → F.obj Y) (𝟙 Y) : F.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
X : C
R : F.RepresentableBy X
X_1 X' : C
f : X_1 ⟶ X'
g : X' ⟶ X
⊢ Eq (α := (F ⋙ uliftFunctor.{w, v}).obj (op X_1))
    ((Equiv.trans R.homEquiv (Equiv.symm Equiv.ulift) : (a : X_1 ⟶ X) → (F ⋙ uliftFunctor.{w, v}).obj (op X_1))
        (f ≫ g) :
      (F ⋙ uliftFunctor.{w, v}).obj (op X_1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ uliftFunctor.{w, v}).map f.op) :
          (a : (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{w, v}).obj (op X'))) →
            (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{w, v}).obj (op X_1)))
        ((Equiv.trans R.homEquiv (Equiv.symm Equiv.ulift) : (a : X' ⟶ X) → (F ⋙ uliftFunctor.{w, v}).obj (op X')) g) :
      (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{w, v}).obj (op X_1)))

Tactic:
simp [R.homEquiv_comp]

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
X : C
R : F.CorepresentableBy X
Y Y' : C
f : Y ⟶ Y'
g : X ⟶ Y
⊢ Eq (α := (F ⋙ uliftFunctor.{w, v}).obj Y')
    ((Equiv.trans R.homEquiv (Equiv.symm Equiv.ulift) : (a : X ⟶ Y') → (F ⋙ uliftFunctor.{w, v}).obj Y') (g ≫ f) :
      (F ⋙ uliftFunctor.{w, v}).obj Y')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ uliftFunctor.{w, v}).map f) :
          (a : (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{w, v}).obj Y)) →
            (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{w, v}).obj Y'))
        ((Equiv.trans R.homEquiv (Equiv.symm Equiv.ulift) : (a : X ⟶ Y) → (F ⋙ uliftFunctor.{w, v}).obj Y) g) :
      (fun (X : Type (max v w)) ↦ X) ((F ⋙ uliftFunctor.{w, v}).obj Y'))

Tactic:
simp [R.homEquiv_comp]

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X_1 : C
R : F.RepresentableBy X_1
X Y : Cᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : obj (obj uliftYoneda.{w, v₁, u₁} X_1) X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj uliftYoneda.{w, v₁, u₁} X_1) f ≫
            Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  ((equivEquivIso :
                        (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                          (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                      (Equiv.trans Equiv.ulift R.homEquiv) :
                    obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
                Y)))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  ((equivEquivIso :
                        (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                          (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                      (Equiv.trans Equiv.ulift R.homEquiv) :
                    obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
                X) ≫
            F.map f))
        x
⊢ Eq (α := obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ⟶ F.obj Y)
    (map (obj uliftYoneda.{w, v₁, u₁} X_1) f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            ((equivEquivIso :
                  (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                    (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
          Y))
    (Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            ((equivEquivIso :
                  (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                    (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
          X) ≫
      F.map f)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X_1 : C
R : F.RepresentableBy X_1
X Y : Cᵒᵖ
f : X ⟶ Y
x : obj (obj uliftYoneda.{w, v₁, u₁} X_1) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj uliftYoneda.{w, v₁, u₁} X_1) f ≫
          Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                ((equivEquivIso :
                      (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                        (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                ((equivEquivIso :
                      (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                        (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
              X) ≫
          F.map f))
      x

Tactic:
R.homEquiv_comp f.unop _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X_1 : C
R : F.RepresentableBy X_1
X Y : Cᵒᵖ
f : X ⟶ Y
x : obj (obj uliftYoneda.{w, v₁, u₁} X_1) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj uliftYoneda.{w, v₁, u₁} X_1) f ≫
          Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                ((equivEquivIso :
                      (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                        (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : Cᵒᵖ) ↦
                ((equivEquivIso :
                      (a : (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≃ F.obj X) →
                        (uliftYoneda.{w, v₁, u₁}.obj X_1).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftYoneda.{w, v₁, u₁} X_1) X ≅ F.obj X))
              X) ≫
          F.map f))
      x

Tactic:
exact R.homEquiv_comp f.unop _

Premises used: Quiver.Hom.unop, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X_1 : C
R : F.CorepresentableBy X_1
X Y : C
f : X ⟶ Y
h :
  ∀ (x : obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  ((equivEquivIso :
                        (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                          (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                      (Equiv.trans Equiv.ulift R.homEquiv) :
                    obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
                Y)))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (X : C) ↦
                  ((equivEquivIso :
                        (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                          (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                      (Equiv.trans Equiv.ulift R.homEquiv) :
                    obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
                X) ≫
            F.map f))
        x
⊢ Eq (α := obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ⟶ F.obj Y)
    (map (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) f ≫
      Iso.hom
        ((fun (X : C) ↦
            ((equivEquivIso :
                  (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                    (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            ((equivEquivIso :
                  (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                    (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                (Equiv.trans Equiv.ulift R.homEquiv) :
              obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
          X) ≫
      F.map f)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X_1 : C
R : F.CorepresentableBy X_1
X Y : C
f : X ⟶ Y
x : obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) f ≫
          Iso.hom
            ((fun (X : C) ↦
                ((equivEquivIso :
                      (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                        (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : C) ↦
                ((equivEquivIso :
                      (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                        (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
              X) ≫
          F.map f))
      x

Tactic:
R.homEquiv_comp f _

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type (max w v₁)
X_1 : C
R : F.CorepresentableBy X_1
X Y : C
f : X ⟶ Y
x : obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) f ≫
          Iso.hom
            ((fun (X : C) ↦
                ((equivEquivIso :
                      (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                        (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
              Y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (X : C) ↦
                ((equivEquivIso :
                      (a : (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≃ F.obj X) →
                        (uliftCoyoneda.{w, v₁, u₁}.obj (op X_1)).obj X ≅ F.obj X)
                    (Equiv.trans Equiv.ulift R.homEquiv) :
                  obj (obj uliftCoyoneda.{w, v₁, u₁} (op X_1)) X ≅ F.obj X))
              X) ≫
          F.map f))
      x

Tactic:
exact R.homEquiv_comp f _

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
e : obj yoneda X ≅ F
⊢ F.IsRepresentable

Tactic:
(representableByEquiv.symm e).isRepresentable

Premises used: CategoryTheory.Functor.representableByEquiv, CategoryTheory.Functor.RepresentableBy.isRepresentable, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ IsRepresentable.{v₁, v₁, u₁} (obj yoneda X)

Tactic:
IsRepresentable.mk' (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.IsRepresentable.mk'
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ IsRepresentable (obj uliftYoneda.{w, v₁, u₁} X)

Tactic:
RepresentableBy.isRepresentable (representableByUliftFunctorEquiv.symm (RepresentableBy.yoneda X))

Premises used: CategoryTheory.Functor.RepresentableBy.yoneda, CategoryTheory.Functor.RepresentableBy.isRepresentable, CategoryTheory.Functor.representableByUliftFunctorEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X : C
e : obj coyoneda (op X) ≅ F
⊢ F.IsCorepresentable

Tactic:
(corepresentableByEquiv.symm e).isCorepresentable

Premises used: CategoryTheory.Functor.corepresentableByEquiv, CategoryTheory.Functor.CorepresentableBy.isCorepresentable, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ IsCorepresentable.{v₁, v₁, u₁} (obj coyoneda X)

Tactic:
IsCorepresentable.mk' (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.IsCorepresentable.mk'
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ IsCorepresentable (obj uliftCoyoneda.{w, v₁, u₁} X)

Tactic:
CorepresentableBy.isCorepresentable
    (corepresentableByUliftFunctorEquiv.symm (CorepresentableBy.coyoneda X))

Premises used: CategoryTheory.Functor.corepresentableByUliftFunctorEquiv, CategoryTheory.Functor.CorepresentableBy.isCorepresentable, CategoryTheory.Functor.CorepresentableBy.coyoneda, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
inst_1 : F.IsRepresentable
X : Cᵒᵖ
f : unop X ⟶ F.reprX
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom F.reprW) X) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj F.reprX).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj X))
        f :
      (fun (X : Type v₁) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj (op F.reprX))) → (fun (X : Type v₁) ↦ X) (F.obj (op (unop X))))
        F.reprx :
      (fun (X : Type v₁) ↦ X) (F.obj (op (unop X))))

Tactic:
apply RepresentableBy.homEquiv_eq

Premises used: CategoryTheory.Functor.RepresentableBy.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max v v₁)
inst_1 : F.IsRepresentable
X : Cᵒᵖ
f : ULift.{v, v₁} (unop X ⟶ F.reprX)
⊢ Eq (α := (fun (X : Type (max v₁ v)) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom F.uliftYonedaReprXIso) X) :
          (a : (fun (X : Type (max v₁ v)) ↦ X) ((uliftYoneda.{v, v₁, u₁}.obj F.reprX).obj X)) →
            (fun (X : Type (max v₁ v)) ↦ X) (F.obj X))
        f :
      (fun (X : Type (max v₁ v)) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.down.op) :
          (a : (fun (X : Type (max v v₁)) ↦ X) (F.obj (op F.reprX))) →
            (fun (X : Type (max v v₁)) ↦ X) (F.obj (op (unop X))))
        F.reprx :
      (fun (X : Type (max v v₁)) ↦ X) (F.obj (op (unop X))))

Tactic:
RepresentableBy.homEquiv_eq _ _

Premises used: CategoryTheory.Functor.reprx, CategoryTheory.Functor.RepresentableBy.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst_1 : F.IsCorepresentable
X : C
f : F.coreprX ⟶ X
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom F.coreprW) X) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op F.coreprX)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj X))
        f :
      (fun (X : Type v₁) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj F.coreprX)) → (fun (X : Type v₁) ↦ X) (F.obj X))
        F.coreprx :
      (fun (X : Type v₁) ↦ X) (F.obj X))

Tactic:
apply CorepresentableBy.homEquiv_eq

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_eq
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Type (max v v₁)
inst_1 : F.IsCorepresentable
X : C
f : ULift.{v, v₁} (F.coreprX ⟶ X)
⊢ Eq (α := (fun (X : Type (max v₁ v)) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom F.uliftCoyonedaCoreprXIso) X) :
          (a : (fun (X : Type (max v₁ v)) ↦ X) ((uliftCoyoneda.{v, v₁, u₁}.obj (op F.coreprX)).obj X)) →
            (fun (X : Type (max v₁ v)) ↦ X) (F.obj X))
        f :
      (fun (X : Type (max v₁ v)) ↦ X) (F.obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.down) :
          (a : (fun (X : Type (max v v₁)) ↦ X) (F.obj F.coreprX)) → (fun (X : Type (max v v₁)) ↦ X) (F.obj X))
        F.coreprx :
      (fun (X : Type (max v v₁)) ↦ X) (F.obj X))

Tactic:
CorepresentableBy.homEquiv_eq _ _

Premises used: CategoryTheory.Functor.CorepresentableBy.homEquiv_eq, CategoryTheory.Functor.coreprx
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
inst_1 : F.IsRepresentable
⊢ (F ⋙ uliftFunctor.{w, v}).IsRepresentable

Tactic:
isRepresentable_comp_uliftFunctor_iff.mpr ‹_›

Premises used: Iff.mpr, CategoryTheory.Functor.isRepresentable_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{v₁, v, u₁, v + 1} C (Type v)
inst_1 : F.IsCorepresentable
⊢ (F ⋙ uliftFunctor.{w, v}).IsCorepresentable

Tactic:
isCorepresentable_comp_uliftFunctor_iff.mpr ‹_›

Premises used: Iff.mpr, CategoryTheory.Functor.isCorepresentable_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
i : F ≅ G
inst_1 : F.IsRepresentable
⊢ G.IsRepresentable

Tactic:
(F.representableBy.ofIso i).isRepresentable

Premises used: CategoryTheory.Functor.RepresentableBy.isRepresentable, CategoryTheory.Functor.RepresentableBy.ofIso, CategoryTheory.Functor.representableBy
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v, u₁, v + 1} C (Type v)
i : F ≅ G
inst_1 : F.IsCorepresentable
⊢ G.IsCorepresentable

Tactic:
(F.corepresentableBy.ofIso i).isCorepresentable

Premises used: CategoryTheory.Functor.CorepresentableBy.isCorepresentable, CategoryTheory.Functor.corepresentableBy, CategoryTheory.Functor.CorepresentableBy.ofIso
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
X : Type v
a : PUnit.{v + 1} ⟶ X
⊢ Eq (α := X) ((id.homEquiv : (a : PUnit.{v + 1} ⟶ X) → X) a : X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) a : (a : PUnit.{v + 1}) → X) PUnit.unit : X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
X : Type v
x : X
a : PUnit.{v + 1}
⊢ (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Equiv.symm id.homEquiv : (a : X) → PUnit.{v + 1} ⟶ X) x) :
        (a : PUnit.{v + 1}) → X)
      a =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ IsCorepresentable (𝟭 (Type v))

Tactic:
Functor.CorepresentableBy.id.isCorepresentable

Premises used: CategoryTheory.Functor.CorepresentableBy.isCorepresentable, CategoryTheory.Functor.CorepresentableBy.id
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
η : obj yoneda X ⟶ F
w :
  ∀ (Y : Cᵒᵖ) (f : obj (obj yoneda X) Y),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (ξ : F.obj (op X)) ↦
                {
                  app := fun (x : Cᵒᵖ) ↦
                    ↾fun (f : obj (obj yoneda X) x) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op f)) :
                          (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op (unop x))))
                        ξ,
                  naturality := ⋯ : NatTrans (obj yoneda X) F })
              ((fun (η : obj yoneda X ⟶ F) ↦
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                        (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) →
                          (fun (X : Type v₁) ↦ X) (F.obj (op X)))
                      (𝟙 X) :
                    (fun (X : Type v₁) ↦ X) (F.obj (op X))))
                η))
            Y))
        f =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y)).toFun f
⊢ (fun (ξ : F.obj (op X)) ↦
        {
          app := fun (x : Cᵒᵖ) ↦
            ↾fun (f : obj (obj yoneda X) x) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op f)) :
                  (a : (fun (X : Type v₁) ↦ X) (F.obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op (unop x))))
                ξ,
          naturality := ⋯ : NatTrans (obj yoneda X) F })
      ((fun (η : obj yoneda X ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
                (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (op X))) → (fun (X : Type v₁) ↦ X) (F.obj (op X)))
              (𝟙 X) :
            (fun (X : Type v₁) ↦ X) (F.obj (op X))))
        η) =
    η

Tactic:
ext Y f