awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) Y
⊢ Eq.{v₁ + 1} (α := obj (obj (evaluation C (Type v₁)) X) Z)
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) f ≫
            Iso.hom
              ((fun (x : C ⥤ Type v₁) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation C (Type v₁) ⋙
                            obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                          X)
                        x))
                Z)))
        g))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : C ⥤ Type v₁) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation C (Type v₁) ⋙
                            obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                          X)
                        x))
                Y) ≫
            map
              (obj
                (evaluation C (Type v₁) ⋙
                  obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                X)
              f))
        g))

Tactic:
simpa using coyonedaEquiv_comp _ _

Premises used: CategoryTheory.coyonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) Y) F
⊢ Eq.{v₁ + 1} (α := obj (obj (evaluation C (Type v₁)) Z) F)
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
              Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (x : C ⥤ Type v₁) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift))) ⋯ :
                      Iso (C := (C ⥤ Type v₁) ⥤ Type (max u₁ v₁)) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                        (obj
                          (evaluation C (Type v₁) ⋙
                            obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                          X)))
                  Z))
            F))
        g))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (x : C ⥤ Type v₁) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift))) ⋯ :
                      Iso (C := (C ⥤ Type v₁) ⥤ Type (max u₁ v₁)) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                        (obj
                          (evaluation C (Type v₁) ⋙
                            obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                          X)))
                  Y) ≫
              map
                (evaluation C (Type v₁) ⋙
                  obj (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))) uliftFunctor.{u₁, v₁})
                f)
            F))
        g))

Tactic:
simpa using (coyonedaEquiv_naturality _ _).symm

Premises used: CategoryTheory.coyonedaEquiv_naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
F : C ⥤ Type u₁
X Y : C
f : X ⟶ Y
h :
  ∀ (a : (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).map f ≫
            Iso.hom
              ((fun (x : C) ↦
                  (Equiv.toIso coyonedaEquiv :
                    (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj
                        x ≅
                      (obj (𝟭 (C ⥤ Type u₁)) F).obj x))
                Y)))
        a =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : C) ↦
                  (Equiv.toIso coyonedaEquiv :
                    (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj
                        x ≅
                      (obj (𝟭 (C ⥤ Type u₁)) F).obj x))
                X) ≫
            (obj (𝟭 (C ⥤ Type u₁)) F).map f))
        a
⊢ (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).map f ≫
      Iso.hom
        ((fun (x : C) ↦
            (Equiv.toIso coyonedaEquiv :
              (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj x ≅
                (obj (𝟭 (C ⥤ Type u₁)) F).obj x))
          Y) =
    Iso.hom
        ((fun (x : C) ↦
            (Equiv.toIso coyonedaEquiv :
              (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj x ≅
                (obj (𝟭 (C ⥤ Type u₁)) F).obj x))
          X) ≫
      (obj (𝟭 (C ⥤ Type u₁)) F).map f

Tactic:
ext a
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
F : C ⥤ Type u₁
X Y : C
f : X ⟶ Y
a : (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).map f ≫
          Iso.hom
            ((fun (x : C) ↦
                (Equiv.toIso coyonedaEquiv :
                  (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj x ≅
                    (obj (𝟭 (C ⥤ Type u₁)) F).obj x))
              Y)))
      a =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : C) ↦
                (Equiv.toIso coyonedaEquiv :
                  (obj (yoneda ⋙ obj (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.rightOp coyoneda)) F).obj x ≅
                    (obj (𝟭 (C ⥤ Type u₁)) F).obj x))
              X) ≫
          (obj (𝟭 (C ⥤ Type u₁)) F).map f))
      a

Tactic:
simp [coyonedaEquiv, ← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.coyonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
obtain : ∀ (g : Y ⟶ X) (hg : f ≫ g = 𝟙 X), IsIso f
⊢ IsIso f

Tactic:
obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id, And.right
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ IsIso f

Tactic:
⟨g, hg, (hf _).1 ?_⟩

Premises used: And.left, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
refine : Eq.{v₁ + 1} (α := X ⟶ Y) ((fun (x : Y ⟶ Y) ↦ f ≫ x) (g ≫ f)) ((fun (x : Y ⟶ Y) ↦ f ≫ x) (𝟙 Y))
⊢ IsIso f

Tactic:
refine ⟨g, hg, (hf _).1 ?_⟩
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ Eq.{v₁ + 1} (α := X ⟶ Y) ((fun (x : Y ⟶ Y) ↦ f ≫ x) (g ≫ f)) ((fun (x : Y ⟶ Y) ↦ f ≫ x) (𝟙 Y))

Tactic:
simp only [Category.comp_id, ← Category.assoc, hg, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x

Tactic:
⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩

Premises used: CategoryTheory.isIso_of_coyoneda_map_bijective, Iff.intro
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
refine : IsIso f → ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : IsIso f
T : C
rw : IsIso.{v₁, v₁ + 1} (X := Y ⟶ T) (Y := X ⟶ T) (↾fun (x : Y ⟶ T) ↦ f ≫ x)
⊢ Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x

Tactic:
rw [bijective_iff_isIso_ofHom]

Premises used: CategoryTheory.bijective_iff_isIso_ofHom
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : IsIso f
T : C
⊢ IsIso.{v₁, v₁ + 1} (X := Y ⟶ T) (Y := X ⟶ T) (↾fun (x : Y ⟶ T) ↦ f ≫ x)

Tactic:
inferInstanceAs (IsIso ((coyoneda.map f.op).app _))

Premises used: _private.0.CategoryTheory.isIso_iff_coyoneda_map_bijective._proof_1
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : IsIso f
T : C
⊢ IsIso.{v₁, v₁ + 1} (X := Y ⟶ T) (Y := X ⟶ T) (↾fun (x : Y ⟶ T) ↦ f ≫ x)

Tactic:
exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
rw :
  (∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x) ↔
    ∀ (c : C), IsIso (X := obj (obj coyoneda (op Y)) c) (NatTrans.app (map coyoneda f.op) c)
⊢ IsIso f ↔ ∀ (c : C), IsIso (X := obj (obj coyoneda (op Y)) c) (NatTrans.app (map coyoneda f.op) c)

Tactic:
rw [isIso_iff_coyoneda_map_bijective]

Premises used: CategoryTheory.isIso_iff_coyoneda_map_bijective
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x) ↔
    ∀ (c : C), IsIso (X := obj (obj coyoneda (op Y)) c) (NatTrans.app (map coyoneda f.op) c)

Tactic:
forall_congr' fun _ ↦ bijective_iff_isIso_ofHom _

Premises used: CategoryTheory.bijective_iff_isIso_ofHom, CategoryTheory.CategoryStruct.comp, forall_congr'
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x) ↔
    ∀ (c : C), IsIso (X := obj (obj coyoneda (op Y)) c) (NatTrans.app (map coyoneda f.op) c)

Tactic:
exact forall_congr' fun _ ↦ bijective_iff_isIso_ofHom _

Premises used: CategoryTheory.bijective_iff_isIso_ofHom, forall_congr'
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F
w :
  ∀ (Y : C) (x : obj (obj yoneda Y) X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : F.obj (unop X)) ↦
                {
                  app := fun (Y : C) ↦
                    ↾fun (y : obj (obj uliftCoyoneda.{w, v₁, u₁} X) Y) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down) :
                          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))) →
                            (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
                        x,
                  naturality := ⋯ : NatTrans (obj uliftCoyoneda.{w, v₁, u₁} X) F })
              ((fun (τ : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F) ↦
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (unop X)) :
                        (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftCoyoneda.{w, v₁, u₁}.obj X).obj (unop X))) →
                          (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X)))
                      { down := 𝟙 (unop X) : ULift.{w, v₁} (obj (obj yoneda (unop X)) X) } :
                    (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))))
                τ))
            Y))
        { down := x : ULift.{w, v₁} (obj (obj yoneda Y) X) } =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app Y)).toFun { down := x : ULift.{w, v₁} (obj (obj yoneda Y) X) }
⊢ (fun (x : F.obj (unop X)) ↦
        {
          app := fun (Y : C) ↦
            ↾fun (y : obj (obj uliftCoyoneda.{w, v₁, u₁} X) Y) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down) :
                  (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
                x,
          naturality := ⋯ : NatTrans (obj uliftCoyoneda.{w, v₁, u₁} X) F })
      ((fun (τ : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (unop X)) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftCoyoneda.{w, v₁, u₁}.obj X).obj (unop X))) →
                  (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X)))
              { down := 𝟙 (unop X) } :
            (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))))
        τ) =
    τ

Tactic:
ext Y ⟨x⟩
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F
Y : C
x : obj (obj yoneda Y) X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : F.obj (unop X)) ↦
              {
                app := fun (Y : C) ↦
                  ↾fun (y : obj (obj uliftCoyoneda.{w, v₁, u₁} X) Y) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down) :
                        (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))) →
                          (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
                      x,
                naturality := ⋯ : NatTrans (obj uliftCoyoneda.{w, v₁, u₁} X) F })
            ((fun (τ : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (unop X)) :
                      (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftCoyoneda.{w, v₁, u₁}.obj X).obj (unop X))) →
                        (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X)))
                    { down := 𝟙 (unop X) : ULift.{w, v₁} (obj (obj yoneda (unop X)) X) } :
                  (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))))
              τ))
          Y))
      { down := x : ULift.{w, v₁} (obj (obj yoneda Y) X) } =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app Y)).toFun { down := x : ULift.{w, v₁} (obj (obj yoneda Y) X) }

Tactic:
simp [← comp_apply, ← τ.naturality]

Premises used: CategoryTheory.comp_apply, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
x : F.obj (unop X)
⊢ (fun (τ : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (unop X)) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftCoyoneda.{w, v₁, u₁}.obj X).obj (unop X))) →
                (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X)))
            { down := 𝟙 (unop X) } :
          (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))))
      ((fun (x : F.obj (unop X)) ↦
          {
            app := fun (Y : C) ↦
              ↾fun (y : obj (obj uliftCoyoneda.{w, v₁, u₁} X) Y) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map y.down) :
                    (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
                  x,
            naturality := ⋯ : NatTrans (obj uliftCoyoneda.{w, v₁, u₁} X) F })
        x) =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type (max w v₁)
f : obj uliftCoyoneda.{w, v₁, u₁} (op X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
        ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) f) :
      (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
    ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F) → F.obj (unop (op Y)))
        (map uliftCoyoneda.{w, v₁, u₁} g.op ≫ f) :
      F.obj (unop (op Y)))

Tactic:
simp [uliftCoyonedaEquiv, ← comp_apply, ← f.naturality]

Premises used: CategoryTheory.uliftCoyonedaEquiv, CategoryTheory.comp_apply, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F G : C ⥤ Type (max w v₁)
α : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ F
β : F ⟶ G
⊢ Eq (α := G.obj (unop X))
    ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ G) → G.obj (unop X)) (α ≫ β) : G.obj (unop X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (β.app (unop X)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (unop X))) → (fun (X : Type (max v₁ w)) ↦ X) (G.obj (unop X)))
        ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (unop X)) α) :
      (fun (X : Type (max v₁ w)) ↦ X) (G.obj (unop X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type (max w v₁)
t : F.obj X
obtain :
  ∀ (u : obj uliftCoyoneda.{w, v₁, u₁} (op X) ⟶ F),
    Eq (α := obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
      ((Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op Y))) → uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
            ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) u)) :
        obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
      (map uliftCoyoneda.{w, v₁, u₁} f.op ≫
          (Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op X))) → uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F)
            ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) u) :
        obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
⊢ Eq (α := obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    ((Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op Y))) → uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
          t) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    (map uliftCoyoneda.{w, v₁, u₁} f.op ≫
        (Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op X))) → uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) t :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)

Tactic:
obtain ⟨u, rfl⟩ := uliftCoyonedaEquiv.surjective t

Premises used: CategoryTheory.uliftCoyonedaEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type (max w v₁)
u : obj uliftCoyoneda.{w, v₁, u₁} (op X) ⟶ F
rw :
  Eq (α := obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    ((Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op Y))) → uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F)
        ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F) → F.obj (unop (op Y)))
          (map uliftCoyoneda.{w, v₁, u₁} f.op ≫ u)) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    (map uliftCoyoneda.{w, v₁, u₁} f.op ≫
        (Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op X))) → uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F)
          ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) u) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
⊢ Eq (α := obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    ((Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op Y))) → uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
          ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) u)) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    (map uliftCoyoneda.{w, v₁, u₁} f.op ≫
        (Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op X))) → uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F)
          ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) u) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)

Tactic:
rw [uliftCoyonedaEquiv_naturality]

Premises used: CategoryTheory.uliftCoyonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type (max w v₁)
u : obj uliftCoyoneda.{w, v₁, u₁} (op X) ⟶ F
⊢ Eq (α := obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    ((Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op Y))) → uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F)
        ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op Y) ⟶ F) → F.obj (unop (op Y)))
          (map uliftCoyoneda.{w, v₁, u₁} f.op ≫ u)) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)
    (map uliftCoyoneda.{w, v₁, u₁} f.op ≫
        (Equiv.symm uliftCoyonedaEquiv : (a : F.obj (unop (op X))) → uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F)
          ((uliftCoyonedaEquiv : (a : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F) → F.obj (unop (op X))) u) :
      obj uliftCoyoneda.{w, v₁, u₁} (op Y) ⟶ F)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (uliftCoyonedaEquiv :
        (a : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ uliftCoyoneda.{w, v₁, u₁}.obj Y) → ULift.{w, v₁} (unop Y ⟶ unop X))
      (map uliftCoyoneda.{w, v₁, u₁} f) =
    { down := f.unop : ULift.{w, v₁} (unop Y ⟶ unop X) }

Tactic:
simp [uliftCoyonedaEquiv, uliftYoneda]

Premises used: CategoryTheory.uliftCoyonedaEquiv, CategoryTheory.uliftYoneda
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ P), p ≫ f = p ≫ g
w :
  ∀ (X : C) (x : P.obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X)).toFun x
⊢ f = g

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : obj uliftCoyoneda.{w, v₁, u₁} X ⟶ P), p ≫ f = p ≫ g
X : C
x : P.obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X)).toFun x

Tactic:
simpa [uliftCoyonedaEquiv]
    using congr_arg uliftCoyonedaEquiv.{w} (h _ (uliftCoyonedaEquiv.symm x))

Premises used: CategoryTheory.uliftCoyonedaEquiv