awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ ∃ (P : ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A)) (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
⟨_, inferInstance, isStrongGenerator hP₁ C, ?_⟩

Premises used: inferInstance, CategoryTheory.Presheaf.isStrongGenerator, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
refine :
  LE.le (α := ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A))
    (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A))
    (isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ)
⊢ ∃ (P : ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A)) (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
refine ⟨_, inferInstance, isStrongGenerator hP₁ C, ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
⊢ isCardinalPresentable.{w, v', u'} A κ G

Tactic:
have := hP₂ _ hG
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
this : isCardinalPresentable.{w, v', u'} A κ G
⊢ IsCardinalPresentable.{w, v', u'} G κ

Tactic:
rw [isCardinalPresentable_iff] at this ⊢

Premises used: CategoryTheory.isCardinalPresentable_iff
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
this : IsCardinalPresentable.{w, v', u'} G κ
⊢ IsCardinalPresentable (C := Functor.{w, v', w, u'} Cᵒᵖ A)
    (freeYoneda (X, Subtype.mk (p := P) G hG).1 (↑(X, Subtype.mk (p := P) G hG).2 : A)) κ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
inst_1 : IsLocallyPresentable.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
obtain :
  ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular),
    IsCardinalLocallyPresentable.{w, v', u'} A κ →
      ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} A
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
inst_1 : IsLocallyPresentable.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalLocallyPresentable.{w, v', u'} A κ
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
⟨κ, inferInstance, inferInstance⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
inst_1 : IsLocallyPresentable.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalLocallyPresentable.{w, v', u'} A κ
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
exact ⟨κ, inferInstance, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
⊢ EssentiallySmall.{w, w, w} J

Tactic:
have := essentiallySmallSelf J
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this : EssentiallySmall.{w, w, w} J
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
refine_1 :
  ∀ (i : J) (g : X ⟶ F.obj i) (hg : g ≫ c.ι.app i = h.r ≫ f),
    ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
      f =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
              (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
          xi
⊢ ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
        xi

Tactic:
obtain ⟨i, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ hc (h.r ≫ f)

Premises used: CategoryTheory.Retract.i, CategoryTheory.Retract.r, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
i : J
g : X ⟶ F.obj i
hg : g ≫ c.ι.app i = h.r ≫ f
⊢ f =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
          (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
      (h.i ≫ g)

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
i : J
g : X ⟶ F.obj i
hg : g ≫ c.ι.app i = h.r ≫ f
⊢ ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
        xi

Tactic:
exact ⟨i, h.i ≫ g, by simp [hg]⟩
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj j)
hf :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
            (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
        j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) j) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj j))
        f₁ :
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
          j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) j) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj j))
        f₂ :
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
          j))
refine_2 : ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f
⊢ ∃ (k : J) (f : j ⟶ k),
    Eq (α := (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj k))
          f₁ :
        (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj k))
          f₂ :
        (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))

Tactic:
dsimp at f₁ f₂ hf ⊢
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
⊢ (h.r ≫ f₁) ≫ c.ι.app j = (h.r ≫ f₂) ≫ c.ι.app j

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
refine_2 :
  ∀ (k : J) (u : j ⟶ k) (hj : (h.r ≫ f₁) ≫ F.map u = (h.r ≫ f₂) ≫ F.map u),
    ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f
⊢ ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f

Tactic:
obtain ⟨k, u, hj⟩ := IsCardinalPresentable.exists_eq_of_isColimit'
        κ hc (h.r ≫ f₁) (h.r ≫ f₂) (by simp [hf])

Premises used: CategoryTheory.Retract.r, CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit', CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
k : J
u : j ⟶ k
hj : (h.r ≫ f₁) ≫ F.map u = (h.r ≫ f₂) ≫ F.map u
⊢ f₁ ≫ F.map u = f₂ ≫ F.map u

Tactic:
simpa [← cancel_epi h.r] using hj

Premises used: CategoryTheory.Retract.r, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
k : J
u : j ⟶ k
hj : (h.r ≫ f₁) ≫ F.map u = (h.r ≫ f₂) ≫ F.map u
⊢ ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f

Tactic:
exact ⟨k, u, by simpa [← cancel_epi h.r] using hj⟩
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
Y X : C
h : Retract Y X
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.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
Y X : C
h : Retract Y X
hX : IsCardinalPresentable.{w, v, u} X κ
⊢ IsCardinalPresentable.{w, v, u} Y κ

Tactic:
h.isCardinalPresentable κ

Premises used: CategoryTheory.Retract.isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Retracts
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
Y X : C
h : Retract Y X
hX : IsCardinalPresentable.{w, v, u} X κ
⊢ IsCardinalPresentable.{w, v, u} Y κ

Tactic:
exact h.isCardinalPresentable κ

Premises used: CategoryTheory.Retract.isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
F : Functor.{v', v, u', u} J C
inst_4 : F.IsDense
κ : Cardinal.{w}
inst_5 : Fact κ.IsRegular
inst_6 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (F.obj j) κ
inst_7 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
Y : J
hY : ⊤ Y
e : F.obj Y ≅ X
⊢ isCardinalPresentable.{w, v, u} C κ X

Tactic:
isCardinalPresentable_of_iso e κ

Premises used: CategoryTheory.isCardinalPresentable_of_iso, CategoryTheory.isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
F : Functor.{v', v, u', u} J C
inst_4 : F.IsDense
κ : Cardinal.{w}
inst_5 : Fact κ.IsRegular
inst_6 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (F.obj j) κ
inst_7 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
Y : J
hY : ⊤ Y
e : F.obj Y ≅ X
⊢ isCardinalPresentable.{w, v, u} C κ X

Tactic:
exact isCardinalPresentable_of_iso e κ

Premises used: CategoryTheory.isCardinalPresentable_of_iso
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
F : Functor.{v', v, u', u} J C
inst_4 : F.IsDense
κ : Cardinal.{w}
inst_5 : Fact κ.IsRegular
inst_6 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (F.obj j) κ
inst_7 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
have :
  ∀ (ip : F.DenseAt X),
    ∃ (J_1 : Type w) (x : SmallCategory J_1) (_ : IsCardinalFiltered J_1 κ),
      (ObjectProperty.map ⊤ F).colimitsOfShape J_1 X
⊢ ∃ (J_1 : Type w) (x : SmallCategory J_1) (_ : IsCardinalFiltered J_1 κ),
    (ObjectProperty.map ⊤ F).colimitsOfShape J_1 X

Tactic:
have ip := F.denseAt X
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
F : Functor.{v', v, u', u} J C
inst_4 : F.IsDense
κ : Cardinal.{w}
inst_5 : Fact κ.IsRegular
inst_6 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (F.obj j) κ
inst_7 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
ip : F.DenseAt X
e : CostructuredArrow F X ≌ SmallModel.{w, v', max u' v} (CostructuredArrow F X) :=
  equivSmallModel (CostructuredArrow F X)
j : SmallModel.{w, v', max u' v} (CostructuredArrow F X)
⊢ ⊤ ((CostructuredArrow.proj F X).obj (e.symm.functor.obj j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
F : Functor.{v', v, u', u} J C
inst_4 : F.IsDense
κ : Cardinal.{w}
inst_5 : Fact κ.IsRegular
inst_6 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (F.obj j) κ
inst_7 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
ip : F.DenseAt X
e : CostructuredArrow F X ≌ SmallModel.{w, v', max u' v} (CostructuredArrow F X) :=
  equivSmallModel (CostructuredArrow F X)
⊢ ∃ (J_1 : Type w) (x : SmallCategory J_1) (_ : IsCardinalFiltered J_1 κ),
    (ObjectProperty.map ⊤ F).colimitsOfShape J_1 X

Tactic:
exact ⟨SmallModel.{w} (CostructuredArrow F X), inferInstance,
      IsCardinalFiltered.of_equivalence κ e,
      ⟨{  diag := _
          ι := _
          isColimit := (F.denseAt X).whiskerEquivalence e.symm
          prop_diag_obj j := ⟨_, by simp, ⟨Iso.refl _⟩⟩ }⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : P.ι.IsDense
inst_4 : LocallySmall.{w, v, u} C
hP : P ≤ isCardinalPresentable C κ
inst_5 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow P.ι X) κ
rw : P.isoClosure.IsCardinalFilteredGenerator κ
⊢ P.IsCardinalFilteredGenerator κ

Tactic:
rw [← ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff]

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : P.ι.IsDense
inst_4 : LocallySmall.{w, v, u} C
hP : P ≤ isCardinalPresentable C κ
inst_5 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow P.ι X) κ
⊢ ∀ (X : P.FullSubcategory), IsCardinalPresentable.{w, v, u} (P.ι.obj X) κ

Tactic:
have (X : P.FullSubcategory) : IsCardinalPresentable (P.ι.obj X) κ := hP _ X.property
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : ObjectProperty.EssentiallySmall.{w, v, u} P
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : P.ι.IsDense
inst_4 : LocallySmall.{w, v, u} C
hP : P ≤ isCardinalPresentable C κ
inst_5 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow P.ι X) κ
this : ∀ (X : P.FullSubcategory), IsCardinalPresentable.{w, v, u} (P.ι.obj X) κ
⊢ P.isoClosure.IsCardinalFilteredGenerator κ

Tactic:
simpa using IsCardinalFilteredGenerator.of_isDense P.ι κ

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.IsCardinalFilteredGenerator.of_isDense
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
X : C
J : Type w
x : SmallCategory J
K : J ⥤ CostructuredArrow (P.colimitsCardinalClosure κ).ι X
hJ : HasCardinalLT (Arrow J) κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J

Tactic:
have := ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure P κ J hJ
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
X : C
J : Type w
x : SmallCategory J
K : J ⥤ CostructuredArrow (P.colimitsCardinalClosure κ).ι X
hJ : HasCardinalLT (Arrow J) κ
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J
⊢ Cocone K

Tactic:
exact colimit.cocone K

Premises used: CategoryTheory.Limits.colimit.cocone
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
X : C
⊢ IsFiltered (CostructuredArrow (P.colimitsCardinalClosure κ).ι X)

Tactic:
isFiltered_of_isCardinalFiltered _ κ

Premises used: CategoryTheory.isFiltered_of_isCardinalFiltered
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
⊢ HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C

Tactic:
have : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C :=
      hasColimitsOfShape_of_equivalence
        (equivSmallModel.{w} (CostructuredArrow (P.colimitsCardinalClosure κ).ι X)).symm