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 Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
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))
⊢ 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 (α := (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))
      ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ coyoneda.obj (op X)) → (coyoneda.obj (op X)).obj Y)
          (map coyoneda g.op) :
        obj (obj coyoneda (op X)) Y) :
    (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))
Tactic: rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]
-- 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
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))
rw₁ :
  Eq (α := (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))
        ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ coyoneda.obj (op X)) → (coyoneda.obj (op X)).obj Y)
            (map coyoneda g.op) :
          obj (obj coyoneda (op X)) Y) :
      (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))
⊢ 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 (α := (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))
  ((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]
-- 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 v₁
t : F.obj X
⊢ Eq (α := obj coyoneda (op Y) ⟶ F)
    ((Equiv.symm coyonedaEquiv : (a : F.obj Y) → coyoneda.obj (op Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
          t) :
      obj coyoneda (op Y) ⟶ F)
    (map coyoneda f.op ≫ (Equiv.symm coyonedaEquiv : (a : F.obj X) → coyoneda.obj (op X) ⟶ F) t :
      obj coyoneda (op Y) ⟶ F)
have obtain : ∀ (u : obj coyoneda (op X) ⟶ F),
  Eq (α := obj coyoneda (op Y) ⟶ F)
    ((Equiv.symm coyonedaEquiv : (a : F.obj Y) → coyoneda.obj (op Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (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) u : F.obj X)) :
      obj coyoneda (op Y) ⟶ F)
    (map coyoneda f.op ≫
        (Equiv.symm coyonedaEquiv : (a : F.obj X) → coyoneda.obj (op X) ⟶ F)
          ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) u) :
      obj coyoneda (op Y) ⟶ F)
Tactic: obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
⊢ ∀ {Y : C × (C ⥤ Type v₁)} (f : (X, F) ⟶ Y),
    Eq (α := obj (coyonedaPairing C) (X, F) ⟶ obj (coyonedaEvaluation C) Y)
      (map (coyonedaPairing C) f ≫
        Iso.hom
          ((fun (x : C × (C ⥤ Type v₁)) ↦
              (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
            Y))
      (Iso.hom
          ((fun (x : C × (C ⥤ Type v₁)) ↦
              (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
            (X, F)) ≫
        map (coyonedaEvaluation C) f)
have this : ∀ (Y : C) (G : C ⥤ Type v₁) (f : (X, F) ⟶ (Y, G)),
  Eq (α := obj (coyonedaPairing C) (X, F) ⟶ obj (coyonedaEvaluation C) (Y, G))
    (map (coyonedaPairing C) f ≫
      Iso.hom
        ((fun (x : C × (C ⥤ Type v₁)) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
          (Y, G)))
    (Iso.hom
        ((fun (x : C × (C ⥤ Type v₁)) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
          (X, F)) ≫
      map (coyonedaEvaluation C) f)
Tactic: (Y, G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
⊢ Eq (α := obj (coyonedaPairing C) (X, F) ⟶ obj (coyonedaEvaluation C) (Y, G))
    (map (coyonedaPairing C) f ≫
      Iso.hom
        ((fun (x : C × (C ⥤ Type v₁)) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
          (Y, G)))
    (Iso.hom
        ((fun (x : C × (C ⥤ Type v₁)) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
          (X, F)) ≫
      map (coyonedaEvaluation C) f)
have h : ∀ (a : obj coyoneda (op X) ⟶ F),
  Eq (α := obj (coyonedaEvaluation C) (Y, G))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (coyonedaPairing C) f ≫
          Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (Y, G))))
      a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (X, F)) ≫
          map (coyonedaEvaluation C) f))
      a)
Tactic: ext (a : coyoneda.obj (op X) ⟶ F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : obj coyoneda (op X) ⟶ F
⊢ Eq (α := obj (coyonedaEvaluation C) (Y, G))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (coyonedaPairing C) f ≫
          Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (Y, G))))
      a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (X, F)) ≫
          map (coyonedaEvaluation C) f))
      a)
have h : Eq.{v₁ + 1} (α := obj (evaluationUncurried C (Type v₁)) (Y, G))
  (ULift.down.{u₁, v₁}
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (coyonedaPairing C) f ≫
          Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (Y, G))))
      a))
  (ULift.down.{u₁, v₁}
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (X, F)) ≫
          map (coyonedaEvaluation C) f))
      a))
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : obj coyoneda (op 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 (coyonedaPairing C) f ≫
            Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (Y, G))))
        a))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (X, F)) ≫
            map (coyonedaEvaluation 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 : X ⟶ Y) → F.obj Y) (f.1 ≫ 𝟙 Y) : 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 : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X) :
        F.obj Y) :
    G.obj Y)
Tactic: dsimp [coyonedaEquiv, coyonedaEvaluation]
-- 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.rightOp coyoneda ⋙ coyoneda) X)
      (obj (evaluation C (Type u₁)) Y))
    (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
              Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                (obj (evaluation C (Type u₁)) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
              Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ 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.rightOp coyoneda ⋙ coyoneda) X) a),
  Eq (α := obj (obj (evaluation C (Type u₁)) Y) a)
    (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 u₁) ↦ Equiv.toIso coyonedaEquiv) sorry :
                    Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ 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 coyonedaEquiv) sorry :
                    Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ 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.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
have 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
Tactic: ext a
-- 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 (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
⊢ IsIso f
have obtain : ∀ (g : Y ⟶ X) (hg : f ≫ g = 𝟙 X), IsIso f
Tactic: obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)
-- 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 (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
g : Y ⟶ X
hg : f ≫ g = 𝟙 X
⊢ IsIso f
have refine : Eq.{v₁ + 1} (α := X ⟶ Y) ((fun (x : Y ⟶ Y) ↦ f ≫ x) (g ≫ f)) ((fun (x : Y ⟶ Y) ↦ f ≫ x) (𝟙 Y))
Tactic: refine ⟨g, hg, (hf _).1 ?_⟩
-- 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 (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
have refine : 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⟩
-- 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 (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
have rw : IsIso.{v₁, v₁ + 1} (X := Y ⟶ T) (Y := X ⟶ T) (↾fun (x : Y ⟶ T) ↦ f ≫ x)
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 coyoneda (op Y)) c) (NatTrans.app (map coyoneda f.op) c)
have 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)
Tactic: rw [isIso_iff_coyoneda_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 uliftCoyoneda.{w, v₁, u₁} X ⟶ F
⊢ (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))))
        τ) =
    τ
have 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 := sorry : 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: ext Y ⟨x⟩
-- 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 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)
have 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)
Tactic: obtain ⟨u, rfl⟩ := uliftCoyonedaEquiv.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 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)
have 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)
Tactic: rw [uliftCoyonedaEquiv_naturality]
-- 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 uliftCoyoneda.{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