awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
Y : Cᵒᵖ
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : (X, F) ⟶ (Y, G)
a : obj yoneda (unop X) ⟶ F
⊢ Eq.{v₁ + 1} (α := obj (evaluationUncurried Cᵒᵖ (Type v₁)) (Y, G))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (yonedaPairing C) f ≫
            Iso.hom
              ((fun (x : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (yonedaPairing C) x ≅ obj (yonedaEvaluation C) x))
                (Y, G))))
        a))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : Cᵒᵖ × Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (yonedaPairing C) x ≅ obj (yonedaEvaluation C) x))
                (X, F)) ≫
            map (yonedaEvaluation C) f))
        a))
have h : Eq (α := G.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.2.app Y) : (a : F.obj Y) → G.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app Y) : (a : unop Y ⟶ unop X) → F.obj Y) (𝟙 (unop Y) ≫ f.1.unop) :
        F.obj Y) :
    G.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.2.app Y) : (a : F.obj Y) → G.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.1) : (a : F.obj X) → F.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) : (a : unop X ⟶ unop X) → F.obj X) (𝟙 (unop X)) :
            F.obj X) :
        F.obj Y) :
    G.obj Y)
Tactic: dsimp [yonedaEvaluation, yonedaEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.op yoneda ⋙ coyoneda) X)
      (obj (evaluation Cᵒᵖ (Type u₁)) Y))
    (map (Functor.op yoneda ⋙ coyoneda) f ≫
      Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (NatIso.ofComponents (fun (x : Cᵒᵖ ⥤ Type u₁) ↦ Equiv.toIso yonedaEquiv) ⋯ :
              Iso (C := (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.op yoneda ⋙ coyoneda) X)
                (obj (evaluation Cᵒᵖ (Type u₁)) X)))
          Y))
    (Iso.hom
        ((fun (X : Cᵒᵖ) ↦
            (NatIso.ofComponents (fun (x : Cᵒᵖ ⥤ Type u₁) ↦ Equiv.toIso yonedaEquiv) ⋯ :
              Iso (C := (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.op yoneda ⋙ coyoneda) X)
                (obj (evaluation Cᵒᵖ (Type u₁)) X)))
          X) ≫
      map (evaluation Cᵒᵖ (Type u₁)) f)
have w : ∀ (a : Cᵒᵖ ⥤ Type u₁) (b : obj (obj (Functor.op yoneda ⋙ coyoneda) X) a),
  Eq (α := obj (obj (evaluation Cᵒᵖ (Type u₁)) Y) a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (map (Functor.op yoneda ⋙ coyoneda) f ≫
            Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (NatIso.ofComponents (fun (x : Cᵒᵖ ⥤ Type u₁) ↦ Equiv.toIso yonedaEquiv) sorry :
                    Iso (C := (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.op yoneda ⋙ coyoneda) X)
                      (obj (evaluation Cᵒᵖ (Type u₁)) X)))
                Y))
          a))
      b)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (NatIso.ofComponents (fun (x : Cᵒᵖ ⥤ Type u₁) ↦ Equiv.toIso yonedaEquiv) sorry :
                    Iso (C := (Cᵒᵖ ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.op yoneda ⋙ coyoneda) X)
                      (obj (evaluation Cᵒᵖ (Type u₁)) X)))
                X) ≫
            map (evaluation Cᵒᵖ (Type u₁)) f)
          a))
      b)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).map f ≫
      Iso.hom
        ((fun (x : Cᵒᵖ) ↦
            (Equiv.toIso yonedaEquiv :
              (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).obj x ≅
                (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).obj x))
          Y) =
    Iso.hom
        ((fun (x : Cᵒᵖ) ↦
            (Equiv.toIso yonedaEquiv :
              (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).obj x ≅
                (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).obj x))
          X) ≫
      (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).map f
have h : ∀ (a : (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).obj X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).map f ≫
          Iso.hom
            ((fun (x : Cᵒᵖ) ↦
                (Equiv.toIso yonedaEquiv :
                  (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) 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 yonedaEquiv :
                  (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).obj x ≅
                    (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).obj x))
              X) ≫
          (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).map f))
      a
Tactic: ext a
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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.op yoneda)) F).obj X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).map f ≫
          Iso.hom
            ((fun (x : Cᵒᵖ) ↦
                (Equiv.toIso yonedaEquiv :
                  (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) 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 yonedaEquiv :
                  (obj (yoneda ⋙ obj (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)) (Functor.op yoneda)) F).obj x ≅
                    (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).obj x))
              X) ≫
          (obj (𝟭 (Cᵒᵖ ⥤ Type u₁)) F).map f))
      a
have h : Eq (α := F.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app Y) : (a : unop Y ⟶ unop X) → F.obj Y) (𝟙 (unop Y) ≫ f.unop) :
    F.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj X) → F.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) : (a : unop X ⟶ unop X) → F.obj X) (𝟙 (unop X))) :
    F.obj Y)
Tactic: dsimp [yonedaEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
⊢ IsIso f
have obtain : ∀ (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y), IsIso f
Tactic: obtain ⟨g, hg : g ≫ f = 𝟙 Y⟩ := (hf Y).2 (𝟙 Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
have refine : IsIso f → ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
Tactic: refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : IsIso f
T : C
⊢ Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
have rw : IsIso.{v₁, v₁ + 1} (X := T ⟶ X) (Y := T ⟶ Y) (↾fun (x : T ⟶ X) ↦ x ≫ f)
Tactic: rw [bijective_iff_isIso_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso (X := obj (obj yoneda X) (op c)) (NatTrans.app (map yoneda f) (op c))
have rw : (∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f) ↔
  ∀ (c : C), IsIso (X := obj (obj yoneda X) (op c)) (NatTrans.app (map yoneda f) (op c))
Tactic: rw [isIso_iff_yoneda_map_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type (max w v₁)
τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F
⊢ (fun (x : F.obj (op X)) ↦
        {
          app := fun (Y : Cᵒᵖ) ↦
            ↾fun (y : obj (obj uliftYoneda.{w, v₁, u₁} X) Y) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op y.down)) :
                  (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) →
                    (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop Y))))
                x,
          naturality := ⋯ : NatTrans (obj uliftYoneda.{w, v₁, u₁} X) F })
      ((fun (τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (op X))) →
                  (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X)))
              { down := 𝟙 (unop (op X)) } :
            (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))))
        τ) =
    τ
have w : ∀ (Y : C) (y : obj (obj yoneda X) (op Y)),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : F.obj (op X)) ↦
              {
                app := fun (Y : Cᵒᵖ) ↦
                  ↾fun (y : obj (obj uliftYoneda.{w, v₁, u₁} X) Y) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op y.down)) :
                        (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) →
                          (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop Y))))
                      x,
                naturality := sorry : NatTrans (obj uliftYoneda.{w, v₁, u₁} X) F })
            ((fun (τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                      (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (op X))) →
                        (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X)))
                    { down := 𝟙 (unop (op X)) : ULift.{w, v₁} (obj (obj yoneda X) (op X)) } :
                  (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))))
              τ))
          (op Y)))
      { down := y : ULift.{w, v₁} (obj (obj yoneda X) (op Y)) } =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op Y)))
      { down := y : ULift.{w, v₁} (obj (obj yoneda X) (op Y)) }
Tactic: ext ⟨Y⟩ ⟨y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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
⊢ Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop 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 uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    (map uliftYoneda.{w, v₁, u₁} f.unop ≫
        (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) t :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
have obtain : ∀ (u : obj uliftYoneda.{w, v₁, u₁} (unop X) ⟶ F),
  Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop 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))
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u)) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    (map uliftYoneda.{w, v₁, u₁} f.unop ≫
        (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F)
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
Tactic: obtain ⟨u, rfl⟩ := uliftYonedaEquiv.surjective t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
u : obj uliftYoneda.{w, v₁, u₁} (unop X) ⟶ F
⊢ Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop 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))
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u)) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    (map uliftYoneda.{w, v₁, u₁} f.unop ≫
        (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F)
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
have rw : Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
  ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F) → F.obj (op (unop Y)))
        (map uliftYoneda.{w, v₁, u₁} f.unop ≫ u)) :
    obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
  (map uliftYoneda.{w, v₁, u₁} f.unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F)
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
    obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
Tactic: rw [uliftYonedaEquiv_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type (max w v₁)
X : Cᵒᵖ
x : F.obj X
f : F ⟶ G
⊢ Eq (α := G.obj (op (unop X)))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) x ≫ f) :
      G.obj (op (unop X)))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : G.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
                (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
            x)) :
      G.obj (op (unop X)))
have rw : Eq (α := G.obj (op (unop X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
          (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) x)) :
    (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
      ((Equiv.symm uliftYonedaEquiv : (a : G.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
              (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
          x)) :
    G.obj (op (unop X)))
Tactic: rw [uliftYonedaEquiv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
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 uliftYoneda.{w, v₁, u₁} X ⟶ P), p ≫ f = p ≫ g
⊢ f = g
have 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
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : obj coyoneda (op X) ⟶ F
⊢ (fun (ξ : F.obj X) ↦
        {
          app := fun (x : C) ↦
            ↾fun (x_1 : obj (obj coyoneda (op X)) x) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1) :
                  (a : (fun (X : Type v₁) ↦ X) (F.obj (unop (op X)))) → (fun (X : Type v₁) ↦ X) (F.obj x))
                ξ,
          naturality := ⋯ : NatTrans (obj coyoneda (op X)) F })
      ((fun (η : obj coyoneda (op X) ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app X) :
                (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj X))
              (𝟙 X) :
            (fun (X : Type v₁) ↦ X) (F.obj X)))
        η) =
    η
have w : ∀ (Y : C) (x : X ⟶ Y),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (ξ : F.obj X) ↦
              {
                app := fun (x : C) ↦
                  ↾fun (x_1 : obj (obj coyoneda (op X)) x) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1) :
                        (a : (fun (X : Type v₁) ↦ X) (F.obj (unop (op X)))) → (fun (X : Type v₁) ↦ X) (F.obj x))
                      ξ,
                naturality := sorry : NatTrans (obj coyoneda (op X)) F })
            ((fun (η : obj coyoneda (op X) ⟶ F) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app X) :
                      (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj X))
                    (𝟙 X) :
                  (fun (X : Type v₁) ↦ X) (F.obj X)))
              η))
          Y))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y)).toFun x
Tactic: ext Y (x : X ⟶ Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) f : F.obj X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ F) → F.obj Y) (map coyoneda g.op ≫ f) : F.obj Y)
have change : Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ≫ F.map g) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
      (𝟙 X) :
    (fun (X : Type v₁) ↦ X) (F.obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
      (g ≫ 𝟙 Y) :
    (fun (X : Type v₁) ↦ X) (F.obj Y))
Tactic: change (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ≫ F.map g) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (g ≫ 𝟙 Y) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
have rw : Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda (op X)) g ≫ f.app Y) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
      (𝟙 X) :
    (fun (X : Type v₁) ↦ X) (F.obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
      (g ≫ 𝟙 Y) :
    (fun (X : Type v₁) ↦ X) (F.obj Y))
Tactic: rw [← f.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ coyoneda.obj (op X)) → (coyoneda.obj (op X)).obj Y) (map coyoneda f.op) =
    f
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map coyoneda f.op) Y) :
      (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op Y)).obj Y)) →
        (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y))
    (𝟙 Y) =
  f
Tactic: rw [coyonedaEquiv_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) f : F.obj X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
have rw : Eq.{v₁ + 1} (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
  ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ F) → F.obj Y) (map coyoneda g.op ≫ f) : F.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
      g :
    (fun (X : Type v₁) ↦ X) (F.obj Y))
Tactic: rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]