awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₁ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₂ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
this : IsFiltered J
y₁ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₁
y₂ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₂
hy₁ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₁ =
    x₁
⊢ (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₂ =
    x₂

Tactic:
simp [y₂]
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₁ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₂ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
this : IsFiltered J
y₁ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₁
y₂ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₂
hy₁ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₁ =
    x₁
⊢ (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₂ =
    x₂

Tactic:
have hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂ := by simp [y₂]
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := c.pt.obj cX.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) : (a : c.pt.obj (X.obj j)) → c.pt.obj cX.pt) x₁ :
      c.pt.obj cX.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) : (a : c.pt.obj (X.obj j)) → c.pt.obj cX.pt) x₂ :
      c.pt.obj cX.pt)
this : IsFiltered J
y₁ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₁
y₂ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₂
hy₁ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₁ =
    x₁
hy₂ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₂ =
    x₂
k : K
⊢ Eq (α := (F.obj k).obj cX.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (cX.ι.app j)) :
          (a : (F.obj k).obj (X.obj j)) → (F.obj k).obj cX.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.π.app k).app (X.obj j)) :
              (a : c.pt.obj (X.obj j)) → (F.obj k).obj (X.obj j))
            x₁ :
          (F.obj k).obj (X.obj j)) :
      (F.obj k).obj cX.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (cX.ι.app j)) :
          (a : (F.obj k).obj (X.obj j)) → (F.obj k).obj cX.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.π.app k).app (X.obj j)) :
              (a : c.pt.obj (X.obj j)) → (F.obj k).obj (X.obj j))
            x₂ :
          (F.obj k).obj (X.obj j)) :
      (F.obj k).obj cX.pt)

Tactic:
simp only [← NatTrans.naturality_apply, h]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
hsurj :
  ∀ (x : (c.pt.mapCocone cX).pt),
    ∃ (i : J) (xi : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
            (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
              (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
          xi
hinj :
  ∀ (i : J) (x y : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
    Eq (α := (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
                (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
            x :
          (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
                (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
            y :
          (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i)) →
      ∃ (k : J) (f : i ⟶ k),
        Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
              x :
            (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
              y :
            (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
⊢ IsColimit (c.pt.mapCocone cX)

Tactic:
apply Types.FilteredColimit.isColimitOf'

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (x : (c.pt.mapCocone cX).pt),
    ∃ (i : J) (xi : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
            (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
              (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
          xi

Tactic:
isColimitMapCocone.surjective c hc κ hK cX hF

Premises used: CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (x : (c.pt.mapCocone cX).pt),
    ∃ (i : J) (xi : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
            (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
              (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
          xi

Tactic:
exact isColimitMapCocone.surjective c hc κ hK cX hF

Premises used: CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
    Eq (α := (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
                (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
            x :
          (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
                (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
            y :
          (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i)) →
      ∃ (k : J) (f : i ⟶ k),
        Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
              x :
            (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
              y :
            (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))

Tactic:
isColimitMapCocone.injective c hc κ hK cX hF

Premises used: CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
    Eq (α := (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
                (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
            x :
          (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
                (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
            y :
          (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i)) →
      ∃ (k : J) (f : i ⟶ k),
        Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
              x :
            (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
                (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
              y :
            (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))

Tactic:
exact isColimitMapCocone.injective c hc κ hK cX hF

Premises used: CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : IsLimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', w', w' + 1} K (Type w')
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), (F.obj k).IsCardinalAccessible κ
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hcX : IsColimit cX
⊢ ∀ (k : K), PreservesColimitsOfShape J (F.obj k)

Tactic:
have := fun k ↦ preservesColimitsOfShape_of_isCardinalAccessible (F.obj k) κ J
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : IsLimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', w', w' + 1} K (Type w')
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), (F.obj k).IsCardinalAccessible κ
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hcX : IsColimit cX
this : ∀ (k : K), PreservesColimitsOfShape J (F.obj k)
⊢ Nonempty (IsColimit (c.pt.mapCocone cX))

Tactic:
⟨Accessible.Limits.isColimitMapCocone c
      (fun Y ↦ isLimitOfPreserves ((evaluation C (Type w')).obj Y) hc) κ hK cX
      (fun k ↦ isColimitOfPreserves (F.obj k) hcX)⟩

Premises used: CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone, Nonempty.intro, CategoryTheory.evaluation, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : IsLimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', w', w' + 1} K (Type w')
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), (F.obj k).IsCardinalAccessible κ
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hcX : IsColimit cX
this : ∀ (k : K), PreservesColimitsOfShape J (F.obj k)
⊢ Nonempty (IsColimit (c.pt.mapCocone cX))

Tactic:
exact ⟨Accessible.Limits.isColimitMapCocone c
      (fun Y ↦ isLimitOfPreserves ((evaluation C (Type w')).obj Y) hc) κ hK cX
      (fun k ↦ isColimitOfPreserves (F.obj k) hcX)⟩
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
k : Kᵒᵖ
dsimp : Functor.IsCardinalAccessible.{w, v, v, u, v + 1} (Functor.obj coyoneda (op (Y.obj (unop k)))) κ
⊢ ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
k : Kᵒᵖ
⊢ Functor.IsCardinalAccessible.{w, v, v, u, v + 1} (Functor.obj coyoneda (op (Y.obj (unop k)))) κ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
⊢ ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ

Tactic:
have (k : Kᵒᵖ) : ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ := by
    dsimp; infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
⊢ HasCardinalLT (Arrow.{v', u'} Kᵒᵖ) κ

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
⊢ IsCardinalPresentable.{w, v, u} c.pt κ

Tactic:
exact Functor.isCardinalAccessible_of_isLimit
    (coyoneda.mapCone c.op) (isLimitOfPreserves _ hc.op) κ (by simpa)

Premises used: CategoryTheory.Functor.isCardinalAccessible_of_isLimit, CategoryTheory.coyoneda, CategoryTheory.Limits.IsColimit.op, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.Cocone.op
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
k : K
dsimp : IsCardinalPresentable (e.functor.obj (Y.obj k)) κ
⊢ IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
k : K
⊢ IsCardinalPresentable (e.functor.obj (Y.obj k)) κ

Tactic:
infer_instance