awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
⊢ IsCardinalFiltered J Cardinal.aleph0

Tactic:
have := (isCardinalFiltered_aleph0_iff.{w} J).2 inferInstance
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
obtain :
  ∀ (α : Type w) (w : PartialOrder α),
    IsCardinalFiltered α Cardinal.aleph0 →
      ∀ (F : α ⥤ J),
        F.Final →
          ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J),
            F.Final
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J), F.Final

Tactic:
obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J .aleph0

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed, Cardinal.aleph0
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h : F.Final
rwa rwa₁ rwa₂ rwa₃ : IsCardinalFiltered α Cardinal.aleph0
⊢ IsFiltered α

Tactic:
rwa [← isCardinalFiltered_aleph0_iff.{w}]
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h : F.Final
⊢ IsFiltered α

Tactic:
have : IsFiltered α := by rwa [← isCardinalFiltered_aleph0_iff.{w}]
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this_1 : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h : F.Final
this : IsFiltered α
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J), F.Final

Tactic:
⟨α, _, IsFiltered.isDirectedOrder _, nonempty, F, inferInstance⟩

Premises used: CategoryTheory.IsFiltered.isDirectedOrder, inferInstance, CategoryTheory.IsFiltered.nonempty, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this_1 : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h : F.Final
this : IsFiltered α
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J), F.Final

Tactic:
exact ⟨α, _, IsFiltered.isDirectedOrder _, nonempty, F, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤

Tactic:
⟨ObjectProperty.ofObj φ, inferInstance, fun X _ ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, inferInstance, Exists.intro, CategoryTheory.ObjectProperty.EssentiallySmall.mk
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
refine : ∀ (X : C), ⊤ X → ObjectProperty.isoClosure.{v, u} (ofObj φ) X
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤

Tactic:
refine ⟨ObjectProperty.ofObj φ, inferInstance, fun X _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
obtain :
  ∀ (J : Type w) (w : SmallCategory J),
    IsCardinalFiltered J κ → ∀ (p : P.ColimitOfShape J X), ObjectProperty.isoClosure.{v, u} (ofObj φ) X
⊢ ObjectProperty.isoClosure.{v, u} (ofObj φ) X

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ := hP.exists_colimitsOfShape X

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : Functor.{w, v, w, u} J P.FullSubcategory := P.lift p.toColimitPresentation (P := P).diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.toColimitPresentation (P := P).diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
⊢ HasColimit p.toColimitPresentation (P := P).diag

Tactic:
have : HasColimit p.diag := ⟨_, p.isColimit⟩
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : Functor.{w, v, w, u} J P.FullSubcategory := P.lift p.toColimitPresentation (P := P).diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.toColimitPresentation (P := P).diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this : HasColimit p.toColimitPresentation (P := P).diag
⊢ HasColimit ((G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι)

Tactic:
have := hasColimit_of_iso iso
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : Functor.{w, v, w, u} J P.FullSubcategory := P.lift p.toColimitPresentation (P := P).diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.toColimitPresentation (P := P).diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this_1 : HasColimit p.toColimitPresentation (P := P).diag
this : HasColimit ((G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι)
i : ι :=
  Sigma.mk (β := fun (J : Type w) ↦
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }) J
    (Sigma.mk (β := fun (x : SmallCategory J) ↦
      { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }) inferInstance
      (Subtype.mk (p := fun (F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory) ↦ HasColimit (F ⋙ e.inverse ⋙ P.ι))
        (G ⋙ e.functor) ⋯))
⊢ ObjectProperty.isoClosure.{v, u} (ofObj φ) X

Tactic:
⟨_, ⟨i⟩, ⟨((IsColimit.precomposeHomEquiv iso _).2
    (p.isColimit)).coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.ObjectProperty.ofObj.mk, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, Equiv.invFun, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : Functor.{w, v, w, u} J P.FullSubcategory := P.lift p.toColimitPresentation (P := P).diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.toColimitPresentation (P := P).diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this_1 : HasColimit p.toColimitPresentation (P := P).diag
this : HasColimit ((G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι)
i : ι :=
  Sigma.mk (β := fun (J : Type w) ↦
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }) J
    (Sigma.mk (β := fun (x : SmallCategory J) ↦
      { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }) inferInstance
      (Subtype.mk (p := fun (F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory) ↦ HasColimit (F ⋙ e.inverse ⋙ P.ι))
        (G ⋙ e.functor) ⋯))
⊢ ObjectProperty.isoClosure.{v, u} (ofObj φ) X

Tactic:
exact ⟨_, ⟨i⟩, ⟨((IsColimit.precomposeHomEquiv iso _).2
    (p.isColimit)).coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
rw : ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤
⊢ ∃ (J : Type (w + 1)) (x : Category.{w, w + 1} J), Nonempty (Equivalence.{v, w, u, w + 1} C J)

Tactic:
rw [exists_equivalence_iff_of_locallySmall]

Premises used: CategoryTheory.exists_equivalence_iff_of_locallySmall
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
obtain :
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.EssentiallySmall.{w, v, u} P →
      ∀ (hP : P.IsCardinalFilteredGenerator κ), ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤

Tactic:
obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ

Premises used: CategoryTheory.HasCardinalFilteredGenerator.exists_generator
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤

Tactic:
hP.essentiallyLarge_top

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top
-- Module: Mathlib.CategoryTheory.Presentable.EssentiallyLarge
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤

Tactic:
exact hP.essentiallyLarge_top

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F

Tactic:
⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩

Premises used: CategoryTheory.Functor.IsFinitelyAccessible, _private.0.CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize.match_1, CategoryTheory.Limits.PreservesFilteredColimitsOfSize, CategoryTheory.Limits.PreservesFilteredColimitsOfSize.mk, Iff.intro, _private.0.CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize.match_2, CategoryTheory.Functor.IsCardinalAccessible.mk
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
refine_1 :
  F.IsFinitelyAccessible →
    ∀ (H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F)
      (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
refine_2 :
  PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F →
    ∀ (H : ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F) (J : Type w)
      [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
simp only [isCardinalFiltered_aleph0_iff] at *

Premises used: CategoryTheory.isCardinalFiltered_aleph0_iff
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
refine_2 : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F

Tactic:
simp only [isCardinalFiltered_aleph0_iff] at *

Premises used: CategoryTheory.isCardinalFiltered_aleph0_iff
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
exact H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
exact H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimits F

Tactic:
IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

Premises used: CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := ObjectProperty.{v, u} C) (isFinitelyPresentable C) (isCardinalPresentable C ℵ₀)

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.isFinitelyPresentable, CategoryTheory.isCardinalPresentable, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsFinitelyPresentable.{w, v, u} X ↔
    PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (Functor.obj coyoneda (op X))

Tactic:
Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

Premises used: CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsFinitelyPresentable.{v, v, u} X ↔ PreservesFilteredColimits.{v, v, u, v + 1} (Functor.obj coyoneda (op X))

Tactic:
Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

Premises used: CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X : C
inst_2 rw : IsFinitelyPresentable.{w, v, u} X
⊢ PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1} (Functor.obj coyoneda (op X))

Tactic:
rw [← isFinitelyPresentable_iff_preservesFilteredColimitsOfSize]

Premises used: CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimitsOfSize
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X : C
inst_2 : IsFinitelyPresentable.{w, v, u} X
⊢ IsFinitelyPresentable.{w, v, u} X

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X : ObjectProperty.FullSubcategory.{v, u} (ObjectProperty.isFinitelyPresentable C)
⊢ IsFinitelyPresentable.{w, v, u} (Functor.obj (ObjectProperty.ι (ObjectProperty.isFinitelyPresentable C)) X)

Tactic:
X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.isFinitelyPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X : C
inst_3 : IsFinitelyPresentable.{w, v, u} X
f : X ⟶ c.pt
⊢ ∃ (j : J) (p : X ⟶ D.obj j), p ≫ c.ι.app j = f

Tactic:
Types.jointly_surjective_of_isColimit (isColimitOfPreserves (coyoneda.obj (op X)) hc) f

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, Opposite.op, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X : C
inst_3 : IsFinitelyPresentable.{w, v, u} X
i j : J
f : X ⟶ D.obj i
g : X ⟶ D.obj j
h : f ≫ c.ι.app i = g ≫ c.ι.app j
⊢ ∃ (k : J) (u : i ⟶ k) (v : j ⟶ k), f ≫ D.map u = g ≫ D.map v

Tactic:
(Types.FilteredColimit.isColimit_eq_iff _ (isColimitOfPreserves (coyoneda.obj (op X)) hc)).mp h

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, Opposite.op, Iff.mp, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
⊢ Nonempty J

Tactic:
have : Nonempty J := IsFiltered.nonempty