awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ IsFiltered.{v₂, u₂} J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
this_1 : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
this : IsFiltered.{v₂, u₂} J
⊢ ∃ (j : J) (u : i ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
(Types.FilteredColimit.isColimit_eq_iff'
    (isColimitOfPreserves (coyoneda.obj (op X)) hc) f₁ f₂).1 hf

Premises used: CategoryTheory.coyoneda, Opposite.op, Iff.mp, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff', CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
this_1 : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
this : IsFiltered.{v₂, u₂} J
⊢ ∃ (j : J) (u : i ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
exact (Types.FilteredColimit.isColimit_eq_iff'
    (isColimitOfPreserves (coyoneda.obj (op X)) hc) f₁ f₂).1 hf

Premises used: CategoryTheory.coyoneda, Opposite.op, Iff.mp, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff', CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
change :
  IsCardinalPresentable.{w, v₁, u₁} X κ ↔
    Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ ↔ Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{t, v₁, u₁} (op X)) κ

Tactic:
change _ ↔ (coyoneda.obj (op X) ⋙ uliftFunctor.{t}).IsCardinalAccessible κ
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ ↔
    Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun J _ _ ↦ ?_⟩⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Functor.IsCardinalAccessible.mk
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
refine :
  Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ →
    ∀ (J : Type w) (x : SmallCategory J),
      IsCardinalFiltered J κ → PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ ↔
    Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ

Tactic:
refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun J _ _ ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁})

Tactic:
have := Functor.preservesColimitsOfShape_of_isCardinalAccessible
    (coyoneda.obj (op X) ⋙ uliftFunctor.{t}) κ J
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁})
⊢ PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
preservesColimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{t, v₁}

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves, CategoryTheory.uliftFunctor
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁})
⊢ PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
exact preservesColimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{t, v₁}
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
e : X ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
⊢ Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{t, v₁, u₁} (op X)) κ

Tactic:
(isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj.{t} X κ).1 inferInstance

Premises used: inferInstance, Iff.mp, CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
X : C
J : Type w
inst_1 : SmallCategory J
p : ColimitPresentation.{w, w, v, u} J X
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
h_1 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (p.diag.obj j) κ
inst_3 : LocallySmall.{w, v, u} C
κ' : Cardinal.{w}
inst_4 : Fact κ'.IsRegular
h : κ ≤ κ'
hJ : HasCardinalLT (Arrow J) κ'
⊢ IsCardinalPresentable.{w, v, u} X κ'

Tactic:
have (k : J) : IsCardinalPresentable (p.diag.obj k) κ' := isCardinalPresentable_of_le _ h
  isCardinalPresentable_of_isColimit _ p.isColimit κ' hJ

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.Cocone.mk, CategoryTheory.isCardinalPresentable_of_le, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.isCardinalPresentable_of_isColimit, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
J : Type w
inst_1 : SmallCategory J
p : P.ColimitOfShape J X
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hP : P ≤ CategoryTheory.isCardinalPresentable C κ
inst_3 : LocallySmall.{w, v, u} C
κ' : Cardinal.{w}
inst_4 : Fact κ'.IsRegular
h : κ ≤ κ'
hJ : HasCardinalLT (Arrow J) κ'
⊢ IsCardinalPresentable.{w, v, u} X κ'

Tactic:
p.toColimitPresentation.isCardinalPresentable κ
    (fun j ↦ hP _ (p.prop_diag_obj j)) _ h hJ

Premises used: CategoryTheory.Limits.ColimitPresentation.isCardinalPresentable, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Functor.obj, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
P' : ObjectProperty.{v, u} C
h₁ : P ≤ P'.isoClosure
h₂ : P' ≤ isCardinalPresentable C κ
X : C
obtain :
  ∀ (J : Type w) (w : SmallCategory J),
    IsCardinalFiltered J κ →
      ∀ (hX : P.colimitsOfShape J X),
        ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X

Tactic:
obtain ⟨J, _, _, hX⟩ := h.exists_colimitsOfShape X

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
P' : ObjectProperty.{v, u} C
h₁ : P ≤ P'.isoClosure
h₂ : P' ≤ isCardinalPresentable C κ
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.colimitsOfShape J X
⊢ P'.colimitsOfShape J X

Tactic:
simpa only [colimitsOfShape_isoClosure] using colimitsOfShape_monotone J h₁ _ hX

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape_isoClosure, CategoryTheory.ObjectProperty.colimitsOfShape_monotone
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
P' : ObjectProperty.{v, u} C
h₁ : P ≤ P'.isoClosure
h₂ : P' ≤ isCardinalPresentable C κ
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.colimitsOfShape J X
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X

Tactic:
exact ⟨J, inferInstance, inferInstance, by
      simpa only [colimitsOfShape_isoClosure] using colimitsOfShape_monotone J h₁ _ hX⟩
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.isoClosure ≤ isCardinalPresentable C κ

Tactic:
simpa only [ObjectProperty.isoClosure_le_iff] using h.le_isCardinalPresentable

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, CategoryTheory.ObjectProperty.isoClosure_le_iff
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.isoClosure.IsCardinalFilteredGenerator κ
⊢ P.isoClosure ≤ P.isoClosure

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
obtain :
  ∀ (J : Type w) (w : SmallCategory J),
    IsCardinalFiltered J κ → ∀ (hX : P.ColimitOfShape J X), IsPresentable.{w, v, u} X
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨J, _, _, ⟨hX⟩⟩ := h.exists_colimitsOfShape X

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
obtain :
  ∀ (κ' : Cardinal.{w}) (h₁ : κ'.IsRegular)
    (h₂ :
      ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun (x : Unit) ↦ Arrow J) (fun (x : Unit) ↦ κ.ord.ToType) i) κ'),
    ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'
⊢ ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'

Tactic:
obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.ToType))
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
h₁ : κ'.IsRegular
h₂ : ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun (x : Unit) ↦ Arrow J) (fun (x : Unit) ↦ κ.ord.ToType) i) κ'
⊢ κ < κ'

Tactic:
simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)

Premises used: Sum.inr, PUnit.unit, hasCardinalLT_iff_cardinal_mk_lt
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
h₁ : κ'.IsRegular
h₂ : ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun (x : Unit) ↦ Arrow J) (fun (x : Unit) ↦ κ.ord.ToType) i) κ'
⊢ ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'

Tactic:
exact ⟨κ', ⟨h₁⟩,
      le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)),
      h₂ (Sum.inl ⟨⟩)⟩
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
obtain :
  ∀ (κ' : Cardinal.{w}),
    Fact κ'.IsRegular → ∀ (le : κ ≤ κ') (hκ' : HasCardinalLT (Arrow J) κ'), IsPresentable.{w, v, u} X
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨κ', _, le, hκ'⟩ : ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'),
      HasCardinalLT (Arrow J) κ' := by
    obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.ToType))
    exact ⟨κ', ⟨h₁⟩,
      le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)),
      h₂ (Sum.inl ⟨⟩)⟩
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
w_2 : Fact κ'.IsRegular
le : κ ≤ κ'
hκ' : HasCardinalLT (Arrow J) κ'
⊢ IsCardinalPresentable.{w, v, u} X κ'

Tactic:
have := hX.isCardinalPresentable h.le_isCardinalPresentable _ le hκ'
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
w_2 : Fact κ'.IsRegular
le : κ ≤ κ'
hκ' : HasCardinalLT (Arrow J) κ'
this : IsCardinalPresentable.{w, v, u} X κ'
⊢ IsPresentable.{w, v, u} X

Tactic:
isPresentable_of_isCardinalPresentable _ κ'

Premises used: CategoryTheory.isPresentable_of_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
w_2 : Fact κ'.IsRegular
le : κ ≤ κ'
hκ' : HasCardinalLT (Arrow J) κ'
this : IsCardinalPresentable.{w, v, u} X κ'
⊢ IsPresentable.{w, v, u} X

Tactic:
exact isPresentable_of_isCardinalPresentable _ κ'

Premises used: CategoryTheory.isPresentable_of_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
obtain :
  ∀ (w : Type w) (w_1 : SmallCategory w),
    IsCardinalFiltered w κ →
      ∀ (hX : P.colimitsOfShape w X), ∃ (J : Type w) (x : Category.{w, w} J), P.colimitsOfShape J X
⊢ ∃ (J : Type w) (x : Category.{w, w} J), P.colimitsOfShape J X

Tactic:
obtain ⟨_, _, _, hX⟩ := h.exists_colimitsOfShape X

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
w : Type w
w_1 : SmallCategory w
w_2 : IsCardinalFiltered w κ
hX : P.colimitsOfShape w X
⊢ ∃ (J : Type w) (x : Category.{w, w} J), P.colimitsOfShape J X

Tactic:
⟨_, _, hX⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
w : Type w
w_1 : SmallCategory w
w_2 : IsCardinalFiltered w κ
hX : P.colimitsOfShape w X
⊢ ∃ (J : Type w) (x : Category.{w, w} J), P.colimitsOfShape J X

Tactic:
exact ⟨_, _, hX⟩
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ isCardinalPresentable C κ = P.retractClosure

Tactic:
le_antisymm (fun X hX ↦ ?_) ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
refine_1 : ∀ (X : C) (hX : isCardinalPresentable.{w, v, u} C κ X), P.retractClosure X
refine_2 : P.retractClosure ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ = P.retractClosure

Tactic:
refine le_antisymm (fun X hX ↦ ?_) ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : isCardinalPresentable.{w, v, u} C κ X
⊢ IsCardinalPresentable.{w, v, u} X κ

Tactic:
rw [isCardinalPresentable_iff] at hX

Premises used: CategoryTheory.isCardinalPresentable_iff
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
refine_1 :
  ∀ (J : Type w) (w : SmallCategory J), IsCardinalFiltered J κ → ∀ (p : P.ColimitOfShape J X), P.retractClosure X
⊢ P.retractClosure X

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

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
⊢ EssentiallySmall.{w, w, w} J

Tactic:
have := essentiallySmall_of_small_of_locallySmall.{w} J
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
refine_1 :
  ∀ (j : J) (f : X ⟶ p.toColimitPresentation (P := P).diag.obj j)
    (hf :
      f ≫ { pt := X, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j =
        𝟙 X),
    P.retractClosure X
⊢ P.retractClosure X

Tactic:
obtain ⟨j, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit (𝟙 X)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.CategoryStruct.id, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
j : J
f : X ⟶ p.toColimitPresentation (P := P).diag.obj j
hf :
  f ≫ { pt := X, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j = 𝟙 X
⊢ P.retractClosure X

Tactic:
⟨_, p.prop_diag_obj j, ⟨{ i := _, r := _, retract := hf}⟩⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Limits.Cocone.mk, Nonempty.intro, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.Cocone.ι, Exists.intro, CategoryTheory.Retract.mk, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.retractClosure, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
j : J
f : X ⟶ p.toColimitPresentation (P := P).diag.obj j
hf :
  f ≫ { pt := X, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j = 𝟙 X
⊢ P.retractClosure X

Tactic:
exact ⟨_, p.prop_diag_obj j, ⟨{ i := _, r := _, retract := hf}⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.retractClosure ≤ isCardinalPresentable C κ

Tactic:
simpa only [ObjectProperty.retractClosure_le_iff] using h.le_isCardinalPresentable

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, CategoryTheory.ObjectProperty.retractClosure_le_iff
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
rw : ObjectProperty.EssentiallySmall.{w, v, u} P.retractClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

Tactic:
rw [h.isPresentable_eq_retractClosure]

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isPresentable_eq_retractClosure
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.retractClosure

Tactic:
infer_instance