awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁)
Y : Cᵒᵖ
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : (X, F) ⟶ (Y, G)
h :
  ∀ (a : obj yoneda (unop X) ⟶ F),
    Eq (α := obj (yonedaEvaluation C) (Y, G))
      (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)
      (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)
⊢ Eq (α := obj (yonedaPairing C) (X, F) ⟶ obj (yonedaEvaluation C) (Y, G))
    (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)))
    (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)

Tactic:
ext (a : yoneda.obj X.unop ⟶ F)

Premises used: CategoryTheory.yoneda, Opposite.unop, CategoryTheory.Functor.obj
-- 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₁)
Y : Cᵒᵖ
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : (X, F) ⟶ (Y, G)
a : obj yoneda (unop X) ⟶ F
h :
  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))
⊢ Eq (α := obj (yonedaEvaluation C) (Y, G))
    (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)
    (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)

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- 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₁)
Y : Cᵒᵖ
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : (X, F) ⟶ (Y, G)
a : obj yoneda (unop X) ⟶ F
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)
⊢ 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))

Tactic:
dsimp [yonedaEvaluation, yonedaEquiv]

Premises used: CategoryTheory.yonedaEvaluation, CategoryTheory.yonedaEquiv
-- 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₁)
Y : Cᵒᵖ
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : (X, F) ⟶ (Y, G)
a : obj yoneda (unop X) ⟶ F
⊢ 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:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
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) ⋯ :
                      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) ⋯ :
                      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)
⊢ 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)

Tactic:
ext a b
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
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) ⋯ :
                    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) ⋯ :
                    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:
simp [yonedaEquiv, ← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.yonedaEquiv
-- 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 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : Y ⟶ Z
g : obj (obj (Functor.op yoneda ⋙ coyoneda) X) Y
⊢ Eq (α :=
    obj
      (obj
        (evaluation Cᵒᵖ (Type v₁) ⋙
          obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
            uliftFunctor.{u₁, v₁})
        X)
      Z)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj (Functor.op yoneda ⋙ coyoneda) X) f ≫
          Iso.hom
            ((fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (obj (Functor.op yoneda ⋙ coyoneda) X) x ≅
                    obj
                      (obj
                        (evaluation Cᵒᵖ (Type v₁) ⋙
                          obj
                            (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                            uliftFunctor.{u₁, v₁})
                        X)
                      x))
              Z)))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (obj (Functor.op yoneda ⋙ coyoneda) X) x ≅
                    obj
                      (obj
                        (evaluation Cᵒᵖ (Type v₁) ⋙
                          obj
                            (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                            uliftFunctor.{u₁, v₁})
                        X)
                      x))
              Y) ≫
          map
            (obj
              (evaluation Cᵒᵖ (Type v₁) ⋙
                obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                  uliftFunctor.{u₁, v₁})
              X)
            f))
      g)

Tactic:
simp [yonedaEquiv]

Premises used: CategoryTheory.yonedaEquiv
-- 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 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
g : obj (obj (Functor.op yoneda ⋙ coyoneda) Y) F
⊢ Eq (α :=
    obj
      (obj
        (evaluation Cᵒᵖ (Type v₁) ⋙
          obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
            uliftFunctor.{u₁, v₁})
        Z)
      F)
    (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 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                        Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))
                      ⋯ :
                    Iso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
                      (obj (Functor.op yoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation Cᵒᵖ (Type v₁) ⋙
                          obj
                            (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                            uliftFunctor.{u₁, v₁})
                        X)))
                Z))
          F))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : Cᵒᵖ) ↦
                  (NatIso.ofComponents
                      (fun (x : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) ↦
                        Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))
                      ⋯ :
                    Iso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁) ⥤ Type (max u₁ v₁))
                      (obj (Functor.op yoneda ⋙ coyoneda) X)
                      (obj
                        (evaluation Cᵒᵖ (Type v₁) ⋙
                          obj
                            (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                            uliftFunctor.{u₁, v₁})
                        X)))
                Y) ≫
            map
              (evaluation Cᵒᵖ (Type v₁) ⋙
                obj (whiskeringRight (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Type v₁) (Type (max u₁ v₁)))
                  uliftFunctor.{u₁, v₁})
              f)
          F))
      g)

Tactic:
simpa [← ULift.down_inj] using (yonedaEquiv_naturality _ _).symm

Premises used: ULift.down_inj, CategoryTheory.yonedaEquiv_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.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
⊢ (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

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.op yoneda)) F).obj X
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)
⊢ 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:
dsimp [yonedaEquiv]

Premises used: CategoryTheory.yonedaEquiv
-- 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.op yoneda)) F).obj X
⊢ 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:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Yoneda
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
obtain : ∀ (g : Y ⟶ X) (hg : g ≫ f = 𝟙 Y), IsIso f
⊢ IsIso f

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

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 (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ IsIso f

Tactic:
exact ⟨g, (hf _).1 (by cat_disch), hg⟩
-- 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 (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f

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

Premises used: CategoryTheory.isIso_of_yoneda_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 (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
⊢ 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⟩
-- 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 := T ⟶ X) (Y := T ⟶ Y) (↾fun (x : T ⟶ X) ↦ x ≫ f)
⊢ Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f

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 := T ⟶ X) (Y := T ⟶ Y) (↾fun (x : T ⟶ X) ↦ x ≫ f)

Tactic:
inferInstanceAs (IsIso ((yoneda.map f).app _))

Premises used: _private.0.CategoryTheory.isIso_iff_yoneda_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 := T ⟶ X) (Y := T ⟶ Y) (↾fun (x : T ⟶ X) ↦ x ≫ f)

Tactic:
exact inferInstanceAs (IsIso ((yoneda.map f).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 (β := 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))
⊢ IsIso 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]

Premises used: CategoryTheory.isIso_iff_yoneda_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 (β := 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:
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 (β := 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:
exact forall_congr' fun _ ↦ (bijective_iff_isIso_ofHom _)

Premises used: CategoryTheory.bijective_iff_isIso_ofHom, forall_congr'