awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : LocallySmall.{max w w', v, u} C
X Y : C
x : X ⟶ Y
w :
  ∀ (x_1 : Cᵒᵖ)
    (x_2 :
      Functor.obj
        (Functor.obj
          (shrinkYoneda.{w, v, u} ⋙
            Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
          X)
        x_1),
    Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w w', v, u} Y) x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Functor.map
                (shrinkYoneda.{w, v, u} ⋙
                  Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
                x ≫
              Iso.hom
                ((fun (X : C) ↦
                    (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
                      Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                        (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                        (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
                  Y))
            x_1))
        x_2)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : C) ↦
                    (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
                      Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                        (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                        (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
                  X) ≫
              Functor.map shrinkYoneda.{max w w', v, u} x)
            x_1))
        x_2)
⊢ Eq (α :=
    Quiver.Hom (V := Cᵒᵖ ⥤ Type (max w w'))
      (Functor.obj
        (shrinkYoneda.{w, v, u} ⋙
          Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
        X)
      (Functor.obj shrinkYoneda.{max w w', v, u} Y))
    (Functor.map
        (shrinkYoneda.{w, v, u} ⋙
          Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
        x ≫
      Iso.hom
        ((fun (X : C) ↦
            (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
              Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
              Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
          X) ≫
      Functor.map shrinkYoneda.{max w w', v, u} x)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : LocallySmall.{max w w', v, u} C
X Y : C
x : X ⟶ Y
x_1 : Cᵒᵖ
x_2 :
  Functor.obj
    (Functor.obj
      (shrinkYoneda.{w, v, u} ⋙
        Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
      X)
    x_1
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w w', v, u} Y) x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map
              (shrinkYoneda.{w, v, u} ⋙
                Functor.obj (Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))) uliftFunctor.{w', w})
              x ≫
            Iso.hom
              ((fun (X : C) ↦
                  (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
                    Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                      (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                      (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
                Y))
          x_1))
      x_2)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (FunctorToTypes.shrinkCompUliftFunctorIso (Functor.obj yoneda X) :
                    Iso (C := Cᵒᵖ ⥤ Type (max w w'))
                      (FunctorToTypes.shrink.{w, v, v, u} (Functor.obj yoneda X) ⋙ uliftFunctor.{w', w})
                      (FunctorToTypes.shrink.{max w w', v, v, u} (Functor.obj yoneda X))))
                X) ≫
            Functor.map shrinkYoneda.{max w w', v, u} x)
          x_1))
      x_2)

Tactic:
simp [shrinkYoneda]

Premises used: CategoryTheory.shrinkYoneda
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
h :
  ∀ (x : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) X_1),
    Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj uliftYoneda.{w', v, u} X) f ≫
            Iso.hom
              ((fun (Y : Cᵒᵖ) ↦
                  (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                    ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
                Y)))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (Y : Cᵒᵖ) ↦
                  (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                    ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
                X_1) ≫
            Functor.map (Functor.obj shrinkYoneda.{max w' v, v, u} X) f))
        x)
⊢ Eq (α :=
    Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) X_1 ⟶
      Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y)
    (Functor.map (Functor.obj uliftYoneda.{w', v, u} X) f ≫
      Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
              ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
          Y))
    (Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
              ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
          X_1) ≫
      Functor.map (Functor.obj shrinkYoneda.{max w' v, v, u} X) f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
x : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) X_1
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj uliftYoneda.{w', v, u} X) f ≫
          Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                  ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                  ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
              X_1) ≫
          Functor.map (Functor.obj shrinkYoneda.{max w' v, v, u} X) f))
      x)

Tactic:
(shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm _ _).symm

Premises used: CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
x : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) X_1
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj uliftYoneda.{w', v, u} X) f ≫
          Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                  ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv)) :
                  ULift.{w', v} (unop Y ⟶ X) ≅ Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} X) Y))
              X_1) ≫
          Functor.map (Functor.obj shrinkYoneda.{max w' v, v, u} X) f))
      x)

Tactic:
exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm _ _).symm

Premises used: CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
g : X ⟶ Y
w :
  ∀ (x : Cᵒᵖ) (x_1 : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) x),
    Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} Y) x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Functor.map uliftYoneda.{w', v, u} g ≫
              Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
                      Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                        (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                  Y))
            x))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
                      Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                        (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                  X) ≫
              Functor.map shrinkYoneda.{max w' v, v, u} g)
            x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
      (Functor.obj shrinkYoneda.{max w' v, v, u} Y))
    (Functor.map uliftYoneda.{w', v, u} g ≫
      Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents
                (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
              Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents
                (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
              Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
          X) ≫
      Functor.map shrinkYoneda.{max w' v, v, u} g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
g : X ⟶ Y
x : Cᵒᵖ
x_1 : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) x
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map uliftYoneda.{w', v, u} g ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
                    Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                      (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
                    Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                      (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                X) ≫
            Functor.map shrinkYoneda.{max w' v, v, u} g)
          x))
      x_1)

Tactic:
(shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm _ _).symm

Premises used: CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
g : X ⟶ Y
x : Cᵒᵖ
x_1 : Functor.obj (Functor.obj uliftYoneda.{w', v, u} X) x
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' v, v, u} Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map uliftYoneda.{w', v, u} g ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
                    Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                      (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents
                      (fun (Y : Cᵒᵖ) ↦ Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.symm shrinkYonedaObjObjEquiv))) ⋯ :
                    Iso (C := Cᵒᵖ ⥤ Type (max w' v)) (Functor.obj uliftYoneda.{w', v, u} X)
                      (Functor.obj shrinkYoneda.{max w' v, v, u} X)))
                X) ≫
            Functor.map shrinkYoneda.{max w' v, v, u} g)
          x))
      x_1)

Tactic:
exact (shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm _ _).symm

Premises used: CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X Y_1 : C
f : X ⟶ Y_1
h :
  ∀
    (g :
      Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
        (Functor.obj shrinkYoneda.{w, v, u} X)),
    Eq (α := Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                    ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                      ULift.{w, v} (unop Y ⟶ X)))
                Y_1)))
        { down := g :
          ULift.{v, w}
            (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
              (Functor.obj shrinkYoneda.{w, v, u} X)) })
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (X : C) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                    ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                      ULift.{w, v} (unop Y ⟶ X)))
                X) ≫
            Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f))
        { down := g :
          ULift.{v, w}
            (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
              (Functor.obj shrinkYoneda.{w, v, u} X)) })
⊢ Eq (α :=
    Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X ⟶
      Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
    (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
              ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                ULift.{w, v} (unop Y ⟶ X)))
          Y_1))
    (Iso.hom
        ((fun (X : C) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
              ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                ULift.{w, v} (unop Y ⟶ X)))
          X) ≫
      Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f)

Tactic:
ext ⟨g⟩
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
Y : Cᵒᵖ
X Y_1 : C
f : X ⟶ Y_1
g : unop Y ⟶ X
⊢ Eq (α := Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1)
    (TypeCat.Fun.toFun (X :=
      Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) f ≫
          Iso.hom
            ((fun (X : C) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                  ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                    ULift.{w, v} (unop Y ⟶ X)))
              Y_1)))
      { down := (Equiv.symm shrinkYonedaObjObjEquiv : (a : unop Y ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj Y) g })
    (TypeCat.Fun.toFun (X :=
      Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (X : C) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm Equiv.ulift))) :
                    ULift.{v, w} (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ≅
                      ULift.{w, v} (unop Y ⟶ X)))
                X) ≫
            Functor.map (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) f) :
        TypeCat.Fun
          (Functor.obj (shrinkYoneda.{w, v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w)) Y ⋙ uliftFunctor.{v, w}) X)
          (Functor.obj (Functor.obj coyoneda Y ⋙ uliftFunctor.{w, v}) Y_1))
      ({ down := (Equiv.symm shrinkYonedaObjObjEquiv : (a : unop Y ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj Y) g } :
        ULift.{v, w}
          (Functor.obj (C := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj (evaluation Cᵒᵖ (Type w)) Y)
            (Functor.obj shrinkYoneda.{w, v, u} X))))

Tactic:
simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]

Premises used: CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
⊢ Functor.IsRepresentable.{w, v, u} (Functor.obj shrinkYoneda.{w, v, u} X)

Tactic:
(shrinkYonedaRepresentableBy X).isRepresentable

Premises used: CategoryTheory.shrinkYonedaRepresentableBy, CategoryTheory.Functor.RepresentableBy.isRepresentable
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i : I
X Y Z : C i
f : X ⟶ Y
g : Y ⟶ Z
⊢ (mk (C := C) f).comp (C := C) (mk (C := C) g) = mk (C := C) (f ≫ g)

Tactic:
rfl

Premises used: CategoryTheory.Sigma.SigmaHom.comp, rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i : I
X : C i
⊢ Functor.obj (incl (C := C) i) X = Sigma.mk (β := fun (i : I) ↦ C i) i X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
i : I
x x_1 : C i
x_2 x_3 : x ⟶ x_1
h :
  Eq (α := Functor.obj (incl (C := C) i) x ⟶ Functor.obj (incl (C := C) i) x_1) (Functor.map (incl (C := C) i) x_2)
    (Functor.map (incl (C := C) i) x_3)
⊢ x_2 = x_3

Tactic:
injection h
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl (C := C) i ⋙ F ⟶ incl (C := C) i ⋙ G
j : I
X Y : C j
f : X ⟶ Y
⊢ Eq (α := F.obj (Sigma.mk (β := fun (i : I) ↦ C i) j X) ⟶ G.obj (Sigma.mk (β := fun (i : I) ↦ C i) j Y))
    (F.map (SigmaHom.mk (C := C) f) ≫
      match (motive := (x : (i : I) × C i) → F.obj x ⟶ G.obj x) Sigma.mk (β := fun (i : I) ↦ C i) j Y with
      | ⟨j, X⟩ => (h j).app X)
    ((match (motive := (x : (i : I) × C i) → F.obj x ⟶ G.obj x) Sigma.mk (β := fun (i : I) ↦ C i) j X with
      | ⟨j, X⟩ => (h j).app X) ≫
      G.map (SigmaHom.mk (C := C) f))

Tactic:
apply (h j).naturality

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl (C := C) i ⋙ F ⟶ incl (C := C) i ⋙ G
i : I
X : C i
⊢ (natTrans (C := C) h).app (Sigma.mk (β := fun (i : I) ↦ C i) i X) = (h i).app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
i : I
X : C i
⊢ descMap (C := C) F (Sigma.mk (β := fun (i : I) ↦ C i) i X) (Sigma.mk (β := fun (i : I) ↦ C i) i X)
      (𝟙 (Sigma.mk (β := fun (i : I) ↦ C i) i X)) =
    𝟙
      (Functor.obj (F ((Sigma.mk (β := fun (i : I) ↦ C i) i X).fst (β := fun (i : I) ↦ C i)))
        ((Sigma.mk (β := fun (i : I) ↦ C i) i X).snd (β := fun (i : I) ↦ C i)))

Tactic:
apply (F i).map_id

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
i : I
X Y : C i
f : X ⟶ Y
Y_1 : C i
g : Y ⟶ Y_1
⊢ descMap (C := C) F (Sigma.mk (β := fun (i : I) ↦ C i) i X) (Sigma.mk (β := fun (i : I) ↦ C i) i Y_1)
      (SigmaHom.mk (C := C) f ≫ SigmaHom.mk (C := C) g) =
    descMap (C := C) F (Sigma.mk (β := fun (i : I) ↦ C i) i X) (Sigma.mk (β := fun (i : I) ↦ C i) i Y)
        (SigmaHom.mk (C := C) f) ≫
      descMap (C := C) F (Sigma.mk (β := fun (i : I) ↦ C i) i Y) (Sigma.mk (β := fun (i : I) ↦ C i) i Y_1)
        (SigmaHom.mk (C := C) g)

Tactic:
apply (F i).map_comp

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sigma.Basic
Goal:
I : Type w₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : (i : I) → Functor.{v₁, v₂, u₁, u₂} (C i) D
i : I
X Y : C i
f : X ⟶ Y
⊢ (desc (C := C) F).map (SigmaHom.mk (C := C) f) = (F i).map f

Tactic:
rfl

Premises used: CategoryTheory.Sigma.descMap, rfl