awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
rw :
  (∀
      (d :
        CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X),
      ∃ (c : J), Nonempty.{v + 1} (d ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)) ∧
    ∀
      {d :
        CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X}
      {c : J} (s s' : d ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c),
      ∃ (c' : J) (t : c ⟶ c'),
        s ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
          s' ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t
⊢ p.toCostructuredArrow (P := isCardinalPresentable C κ).Final

Tactic:
rw [Functor.final_iff_of_isFiltered]

Premises used: CategoryTheory.Functor.final_iff_of_isFiltered
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
⊢ (∀
      (d :
        CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X),
      ∃ (c : J), Nonempty.{v + 1} (d ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)) ∧
    ∀
      {d :
        CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X}
      {c : J} (s s' : d ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c),
      ∃ (c' : J) (t : c ⟶ c'),
        s ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
          s' ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t

Tactic:
⟨fun f ↦ ?_, fun {f j} g₁ g₂ ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
refine_1 :
  ∀
    (f :
      CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
        (ObjectProperty.ι (isCardinalPresentable C κ)) X),
    ∃ (c : J), Nonempty.{v + 1} (f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)
refine_2 :
  ∀
    {f :
      CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
        (ObjectProperty.ι (isCardinalPresentable C κ)) X}
    {j : J} (g₁ g₂ : f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj j),
    ∃ (c' : J) (t : j ⟶ c'),
      g₁ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
        g₂ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t
⊢ (∀
      (d :
        CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X),
      ∃ (c : J), Nonempty.{v + 1} (d ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)) ∧
    ∀
      {d :
        CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X}
      {c : J} (s s' : d ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c),
      ∃ (c' : J) (t : c ⟶ c'),
        s ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
          s' ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t

Tactic:
refine ⟨fun f ↦ ?_, fun {f j} g₁ g₂ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
f :
  CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X
refine_1 :
  ∀ (j : J)
    (g :
      Functor.obj (ObjectProperty.ι (isCardinalPresentable C κ)) f.left ⟶
        p.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j)
    (hg :
      g ≫
          { pt := X, ι := p.toColimitPresentation (P := isCardinalPresentable C κ).ι :
                  Cocone p.toColimitPresentation (P := isCardinalPresentable C κ).diag }.ι.app
            j =
        f.hom),
    ∃ (c : J), Nonempty.{v + 1} (f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)
⊢ ∃ (c : J), Nonempty.{v + 1} (f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)

Tactic:
obtain ⟨j, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit f.hom

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.CostructuredArrow.hom, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
f :
  CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X
j : J
g :
  Functor.obj (ObjectProperty.ι (isCardinalPresentable C κ)) f.left ⟶
    p.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j
hg :
  g ≫
      { pt := X, ι := p.toColimitPresentation (P := isCardinalPresentable C κ).ι :
              Cocone p.toColimitPresentation (P := isCardinalPresentable C κ).diag }.ι.app
        j =
    f.hom
⊢ ∃ (c : J), Nonempty.{v + 1} (f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)

Tactic:
⟨j, ⟨CostructuredArrow.homMk (ObjectProperty.homMk g)⟩⟩

Premises used: CategoryTheory.CostructuredArrow.homMk, Nonempty.intro, CategoryTheory.ObjectProperty.homMk, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
f :
  CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X
j : J
g :
  Functor.obj (ObjectProperty.ι (isCardinalPresentable C κ)) f.left ⟶
    p.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j
hg :
  g ≫
      { pt := X, ι := p.toColimitPresentation (P := isCardinalPresentable C κ).ι :
              Cocone p.toColimitPresentation (P := isCardinalPresentable C κ).diag }.ι.app
        j =
    f.hom
⊢ ∃ (c : J), Nonempty.{v + 1} (f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj c)

Tactic:
exact ⟨j, ⟨CostructuredArrow.homMk (ObjectProperty.homMk g)⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
f :
  CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj j
refine_2 :
  ∀ (k : J) (a : j ⟶ k)
    (h :
      g₁.left.hom ≫ p.toColimitPresentation (P := isCardinalPresentable C κ).diag.map a =
        g₂.left.hom ≫ p.toColimitPresentation (P := isCardinalPresentable C κ).diag.map a),
    ∃ (c' : J) (t : j ⟶ c'),
      g₁ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
        g₂ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t
⊢ ∃ (c' : J) (t : j ⟶ c'),
    g₁ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
      g₂ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t

Tactic:
obtain ⟨k, a, h⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ p.isColimit
      g₁.left.hom g₂.left.hom ((CostructuredArrow.w g₁).trans (CostructuredArrow.w g₂).symm)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.CostructuredArrow.w, CategoryTheory.CommaMorphism.left, CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit', CategoryTheory.InducedCategory.Hom.hom, Eq.symm, Eq.trans, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this : IsFiltered.{v', u'} J
f :
  CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow (P := isCardinalPresentable C κ).obj j
k : J
a : j ⟶ k
h :
  g₁.left.hom ≫ p.toColimitPresentation (P := isCardinalPresentable C κ).diag.map a =
    g₂.left.hom ≫ p.toColimitPresentation (P := isCardinalPresentable C κ).diag.map a
⊢ ∃ (c' : J) (t : j ⟶ c'),
    g₁ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t =
      g₂ ≫ p.toCostructuredArrow (P := isCardinalPresentable C κ).map t

Tactic:
exact ⟨k, a, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
X : C
obtain :
  ∀ (J : Type w) (w : SmallCategory J),
    IsCardinalFiltered J κ →
      ∀ (p : ObjectProperty.ColimitOfShape.{w, w, v, u} (isCardinalPresentable C κ) J X),
        Functor.isDenseAt.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
          (ObjectProperty.ι (isCardinalPresentable C κ)) X
⊢ Functor.isDenseAt.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ :=
      (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape, CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : ObjectProperty.ColimitOfShape.{w, w, v, u} (isCardinalPresentable C κ) J X
⊢ Functor.isDenseAt.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X

Tactic:
⟨(Functor.Final.isColimitWhiskerEquiv (F := p.toCostructuredArrow) _).1
      (IsColimit.ofIsoColimit p.isColimit (Cocone.ext (Iso.refl _)))⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Functor.isDenseAt, CategoryTheory.Iso.refl, Equiv.toFun, Nonempty.intro, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : ObjectProperty.ColimitOfShape.{w, w, v, u} (isCardinalPresentable C κ) J X
⊢ Functor.isDenseAt.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
    (ObjectProperty.ι (isCardinalPresentable C κ)) X

Tactic:
exact ⟨(Functor.Final.isColimitWhiskerEquiv (F := p.toCostructuredArrow) _).1
      (IsColimit.ofIsoColimit p.isColimit (Cocone.ext (Iso.refl _)))⟩
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
X : C
obtain :
  ∀ (J : Type w) (w : SmallCategory J),
    IsCardinalFiltered J κ →
      ∀ (p : ObjectProperty.ColimitOfShape.{w, w, v, u} (isCardinalPresentable C κ) J X),
        IsCardinalFiltered
          (CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
            (ObjectProperty.ι (isCardinalPresentable C κ)) X)
          κ
⊢ IsCardinalFiltered
    (CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
      (ObjectProperty.ι (isCardinalPresentable C κ)) X)
    κ

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ :=
    (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape, CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : ObjectProperty.ColimitOfShape.{w, w, v, u} (isCardinalPresentable C κ) J X
⊢ IsCardinalFiltered
    (CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
      (ObjectProperty.ι (isCardinalPresentable C κ)) X)
    κ

Tactic:
IsCardinalFiltered.of_final p.toCostructuredArrow κ

Premises used: CategoryTheory.IsCardinalFiltered.of_final, CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : ObjectProperty.ColimitOfShape.{w, w, v, u} (isCardinalPresentable C κ) J X
⊢ IsCardinalFiltered
    (CostructuredArrow.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C κ))
      (ObjectProperty.ι (isCardinalPresentable C κ)) X)
    κ

Tactic:
exact IsCardinalFiltered.of_final p.toCostructuredArrow κ

Premises used: CategoryTheory.IsCardinalFiltered.of_final, CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
rw :
  IsCardinalFiltered
    (CostructuredArrow.{v, v, u, u} (C :=
      ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C Cardinal.aleph0))
      (ObjectProperty.ι (isCardinalPresentable C Cardinal.aleph0)) X)
    Cardinal.aleph0
⊢ IsFiltered
    (CostructuredArrow.{v, v, u, u} (C :=
      ObjectProperty.FullSubcategory.{v, u} (ObjectProperty.isFinitelyPresentable C))
      (ObjectProperty.ι (ObjectProperty.isFinitelyPresentable C)) X)

Tactic:
rw [← CategoryTheory.isCardinalFiltered_aleph0_iff.{w},
    ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable]

Premises used: CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
⊢ IsCardinalFiltered
    (CostructuredArrow.{v, v, u, u} (C :=
      ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C Cardinal.aleph0))
      (ObjectProperty.ι (isCardinalPresentable C Cardinal.aleph0)) X)
    Cardinal.aleph0

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsFinitelyAccessibleCategory.{w, v, u} C
⊢ Functor.IsDense.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (isCardinalPresentable C Cardinal.aleph0))
    (ObjectProperty.ι (isCardinalPresentable C Cardinal.aleph0))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsFinitelyAccessibleCategory.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C Cardinal.aleph0)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h : D.IsTerminal e
⊢ D.P e

Tactic:
D.src (h.prop_id)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.src, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop_id
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h : D.IsTerminal e
⊢ h.lift ⋯ = 𝟙 e

Tactic:
h.uniq _ h.prop_id

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop_id, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.uniq
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₁ h₂ : D.IsTerminal e
h : ∀ (j : J) (hj : D.P j), h₁.lift hj = h₂.lift hj
⊢ @lift J inst κ D e h₁ = @lift J inst κ D e h₂

Tactic:
ext j hj
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₁ h₂ : D.IsTerminal e
j : J
hj : D.P j
⊢ h₁.lift hj = h₂.lift hj

Tactic:
h₁.uniq hj (h₂.hlift hj)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.hlift, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.uniq
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₁ h₂ : D.IsTerminal e
j : J
hj : D.P j
⊢ h₁.lift hj = h₂.lift hj

Tactic:
exact h₁.uniq hj (h₂.hlift hj)

Premises used: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.hlift, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.uniq
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₁ h₂ : D.IsTerminal e
⊢ @lift J inst κ D e h₁ = @lift J inst κ D e h₂

Tactic:
have : @h₁.lift = @h₂.lift := by
      ext j hj
      exact h₁.uniq hj (h₂.hlift hj)
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₁ h₂ : D.IsTerminal e
this : @lift J inst κ D e h₁ = @lift J inst κ D e h₂
mk :
  ∀ (prop_id : D.W (𝟙 e)) (lift : {j : J} → (hj : D.P j) → j ⟶ e) (hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj))
    (uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ), lift hj = φ)
    (comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift ⋯ = lift ⋯)
    (this :
      @IsTerminal.lift J inst κ D e
          { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } =
        @IsTerminal.lift J inst κ D e h₂),
    { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } = h₂
⊢ h₁ = h₂

Tactic:
cases h₁
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₂ : D.IsTerminal e
prop_id : D.W (𝟙 e)
lift : {j : J} → (hj : D.P j) → j ⟶ e
hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)
uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ), lift hj = φ
comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift ⋯ = lift ⋯
this :
  @IsTerminal.lift J inst κ D e
      { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } =
    @IsTerminal.lift J inst κ D e h₂
mk :
  ∀ (prop_id_1 : D.W (𝟙 e)) (lift_1 : {j : J} → (hj : D.P j) → j ⟶ e)
    (hlift_1 : ∀ {j : J} (hj : D.P j), D.W (lift_1 hj))
    (uniq_1 : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ), lift_1 hj = φ)
    (comm_1 : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift_1 ⋯ = lift_1 ⋯)
    (this :
      @IsTerminal.lift J inst κ D e
          { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } =
        @IsTerminal.lift J inst κ D e
          { prop_id := prop_id_1, lift := @lift_1, hlift := @hlift_1, uniq := @uniq_1, comm := @comm_1 }),
    { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } =
      { prop_id := prop_id_1, lift := @lift_1, hlift := @hlift_1, uniq := @uniq_1, comm := @comm_1 }
⊢ { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } = h₂

Tactic:
cases h₂
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
lift : {j : J} → (hj : D.P j) → j ⟶ e
hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)
uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ), lift hj = φ
comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift ⋯ = lift ⋯
prop_id_1 : D.W (𝟙 e)
lift_1 : {j : J} → (hj : D.P j) → j ⟶ e
hlift_1 : ∀ {j : J} (hj : D.P j), D.W (lift_1 hj)
uniq_1 : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ), lift_1 hj = φ
comm_1 : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift_1 ⋯ = lift_1 ⋯
this :
  @IsTerminal.lift J inst κ D e
      { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } =
    @IsTerminal.lift J inst κ D e
      { prop_id := prop_id_1, lift := @lift_1, hlift := @hlift_1, uniq := @uniq_1, comm := @comm_1 }
⊢ { prop_id := prop_id, lift := @lift, hlift := @hlift, uniq := @uniq, comm := @comm : D.IsTerminal e } =
    { prop_id := prop_id_1, lift := @lift_1, hlift := @hlift_1, uniq := @uniq_1, comm := @comm_1 }

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Presentable.Directed
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ (lift : j ⟶ e), D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ (li : i ⟶ e) (lj : j ⟶ e), D.W li ∧ D.W lj ∧ f ≫ lj = li
i j : J
x : i ⟶ j
hf : D.W x
obtain :
  ∀ (li : i ⟶ e) (lj : j ⟶ e) (hli : D.W li) (hlj : D.W lj) (fac : x ≫ lj = li),
    x ≫ ⋯.choose (p := D.W) = ⋯.choose (p := D.W)
⊢ x ≫ ⋯.choose (p := D.W) = ⋯.choose (p := D.W)

Tactic:
obtain ⟨li, lj, hli, hlj, fac⟩ := h₃ _ hf