awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
rw :
  ∀ (G : C),
    P G →
      ∀
        (g₁ g₂ :
          G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
        Eq (α := G ⟶ (E.coconeAt X).pt)
            (g₁ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X))
            (g₂ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X)) →
          g₁ = g₂
⊢ Mono (X := colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)) (Y :=
    (E.coconeAt X).pt)
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))

Tactic:
rw [hS₁.isSeparating.mono_iff]

Premises used: CategoryTheory.ObjectProperty.IsSeparating.mono_iff, CategoryTheory.ObjectProperty.IsStrongGenerator.isSeparating
-- 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
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
G₁ :
  ∀ (g₁ : G ⟶ colimit Φ)
    (g₂ : G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
    Eq (α := G ⟶ (E.coconeAt X).pt)
        (g₁ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X))
        (g₂ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X)) →
      g₁ = g₂
⊢ ∀ (g₁ g₂ : G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
    Eq (α := G ⟶ (E.coconeAt X).pt)
        (g₁ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X))
        (g₂ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X)) →
      g₁ = g₂

Tactic:
(g₁ : G ⟶ colimit Φ)
-- 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
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ : G ⟶ colimit Φ
G₁ :
  ∀ (g₂ : G ⟶ colimit Φ),
    Eq (α := G ⟶ (E.coconeAt X).pt)
        (g₁ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X))
        (g₂ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X)) →
      g₁ = g₂
⊢ ∀ (g₂ : G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
    Eq (α := G ⟶ (E.coconeAt X).pt)
        (g₁ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X))
        (g₂ ≫
          colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
            (E.coconeAt X)) →
      g₁ = g₂

Tactic:
(g₂ : G ⟶ colimit Φ)
-- 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
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
g₃ :
  ∀ (h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))),
    g₁ = g₂
⊢ Eq (α := G ⟶ (E.coconeAt X).pt)
      (g₁ ≫
        colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
          (E.coconeAt X))
      (g₂ ≫
        colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
          (E.coconeAt X)) →
    g₁ = g₂

Tactic:
(h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X))
-- 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
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
⊢ IsCardinalPresentable.{w, v, u} G κ

Tactic:
have : IsCardinalPresentable G κ := hS₂ _ hG
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
this : IsCardinalPresentable.{w, v, u} G κ
obtain :
  ∀ (j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (f₁ : G ⟶ Φ.obj j₁)
    (hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁),
    ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
      φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂
⊢ ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
    φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂

Tactic:
obtain ⟨j₁, f₁, hf₁⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₁

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
this : IsCardinalPresentable.{w, v, u} G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
obtain :
  ∀ (j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (f₂ : G ⟶ Φ.obj j₂)
    (hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂),
    ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
      φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂
⊢ ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
    φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂

Tactic:
obtain ⟨j₂, f₂, hf₂⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₂

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
this : IsCardinalPresentable.{w, v, u} G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ CategoryStruct.comp (Y := Φ.obj (IsFiltered.max j₁ j₂)) (f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂))
      (colimit.ι Φ (IsFiltered.max j₁ j₂)) =
    g₁

Tactic:
simpa
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
this : IsCardinalPresentable.{w, v, u} G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ CategoryStruct.comp (Y := Φ.obj (IsFiltered.max j₁ j₂)) (f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂))
      (colimit.ι Φ (IsFiltered.max j₁ j₂)) =
    g₂

Tactic:
simpa
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
this : IsCardinalPresentable.{w, v, u} G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
    φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂

Tactic:
exact ⟨IsFiltered.max j₁ j₂, f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂),
          f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂), by simpa, by simpa⟩
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : Eq (α := G ⟶ (E.coconeAt X).pt) (g₁ ≫ colimit.desc Φ (E.coconeAt X)) (g₂ ≫ colimit.desc Φ (E.coconeAt X))
this : IsCardinalPresentable.{w, v, u} G κ
obtain :
  ∀ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X) (φ₁ φ₂ : G ⟶ Φ.obj j)
    (h :
      Eq (α := G ⟶ (E.coconeAt X).pt)
        (CategoryStruct.comp (Y := colimit Φ) (φ₁ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
        (CategoryStruct.comp (Y := colimit Φ) (φ₂ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))),
    Eq (α := G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
      (φ₁ ≫ colimit.ι Φ j) (φ₂ ≫ colimit.ι Φ j)
⊢ g₁ = g₂

Tactic:
obtain ⟨j, φ₁, φ₂, rfl, rfl⟩ :
          ∃ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X)
            (φ₁ φ₂ : G ⟶ Φ.obj j), φ₁ ≫ colimit.ι _ _ = g₁ ∧ φ₂ ≫ colimit.ι _ _ = g₂ := by
        obtain ⟨j₁, f₁, hf₁⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₁
        obtain ⟨j₂, f₂, hf₂⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₂
        exact ⟨IsFiltered.max j₁ j₂, f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂),
          f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂), by simpa, by simpa⟩

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure, CategoryTheory.ObjectProperty.ι, CategoryTheory.CostructuredArrow, rfl, CategoryTheory.Limits.colimit.ι
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable.{w, v, u} G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h :
  Eq (α := G ⟶ (E.coconeAt X).pt)
    (CategoryStruct.comp (Y := colimit Φ) (φ₁ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
    (CategoryStruct.comp (Y := colimit Φ) (φ₂ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
hJ : HasCardinalLT (Arrow WalkingParallelPair) κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair

Tactic:
apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable.{w, v, u} G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h :
  Eq (α := G ⟶ (E.coconeAt X).pt)
    (CategoryStruct.comp (Y := colimit Φ) (φ₁ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
    (CategoryStruct.comp (Y := colimit Φ) (φ₂ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
⊢ HasCardinalLT (Arrow WalkingParallelPair) κ

Tactic:
.of_le ?_ (Cardinal.IsRegular.aleph0_le Fact.out)

Premises used: Cardinal.IsRegular.aleph0_le, HasCardinalLT.of_le, Fact.out
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable.{w, v, u} G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h :
  Eq (α := G ⟶ (E.coconeAt X).pt)
    (CategoryStruct.comp (Y := colimit Φ) (φ₁ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
    (CategoryStruct.comp (Y := colimit Φ) (φ₂ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
hJ : HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0
⊢ HasCardinalLT (Arrow WalkingParallelPair) κ

Tactic:
refine .of_le ?_ (Cardinal.IsRegular.aleph0_le Fact.out)
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable.{w, v, u} G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h :
  Eq (α := G ⟶ (E.coconeAt X).pt)
    (CategoryStruct.comp (Y := colimit Φ) (φ₁ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
    (CategoryStruct.comp (Y := colimit Φ) (φ₂ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
hJ : Finite (Arrow WalkingParallelPair)
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

Tactic:
simp only [hasCardinalLT_aleph0_iff]

Premises used: hasCardinalLT_aleph0_iff
-- 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
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this : IsCardinalPresentable.{w, v, u} G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h :
  Eq (α := G ⟶ (E.coconeAt X).pt)
    (CategoryStruct.comp (Y := colimit Φ) (φ₁ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
    (CategoryStruct.comp (Y := colimit Φ) (φ₂ ≫ colimit.ι Φ j) (colimit.desc Φ (E.coconeAt X)))
⊢ Finite (Arrow WalkingParallelPair)

Tactic:
infer_instance