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_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)))
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair

Tactic:
have : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair := by
        apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure
        refine .of_le ?_ (Cardinal.IsRegular.aleph0_le Fact.out)
        simp only [hasCardinalLT_aleph0_iff]
        infer_instance
-- 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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
hF : ∀ (j_1 : WalkingParallelPair), P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj j_1)
⊢ P.colimitsCardinalClosure κ (coequalizer φ₁ φ₂)

Tactic:
apply ObjectProperty.prop_colimit

Premises used: CategoryTheory.ObjectProperty.prop_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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj WalkingParallelPair.zero)

Tactic:
P.le_colimitsCardinalClosure _ _ hG

Premises used: CategoryTheory.ObjectProperty.le_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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj WalkingParallelPair.zero)

Tactic:
exact P.le_colimitsCardinalClosure _ _ hG

Premises used: CategoryTheory.ObjectProperty.le_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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj WalkingParallelPair.one)

Tactic:
j.left.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.CostructuredArrow.left
-- 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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
⊢ P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj WalkingParallelPair.one)

Tactic:
exact j.left.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.CostructuredArrow.left
-- 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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory :=
  FullSubcategory.mk (P := P.colimitsCardinalClosure κ) (coequalizer φ₁ φ₂) ⋯
⊢ φ₁ ≫ (E.coconeAt X).ι.app j = φ₂ ≫ (E.coconeAt X).ι.app j

Tactic:
simpa using h
-- 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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory :=
  FullSubcategory.mk (P := P.colimitsCardinalClosure κ) (coequalizer φ₁ φ₂) ⋯
a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X := coequalizer.desc ((E.coconeAt X).ι.app j) ⋯
⊢ (P.colimitsCardinalClosure κ).ι.map (homMk (P := P.colimitsCardinalClosure κ) (coequalizer.π φ₁ φ₂)) ≫
      (CostructuredArrow.mk a).hom =
    j.hom

Tactic:
simp [E, a]
-- 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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory :=
  FullSubcategory.mk (P := P.colimitsCardinalClosure κ) (coequalizer φ₁ φ₂) ⋯
a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X := coequalizer.desc ((E.coconeAt X).ι.app j) ⋯
ψ : j ⟶ CostructuredArrow.mk a :=
  CostructuredArrow.homMk (homMk (P := P.colimitsCardinalClosure κ) (coequalizer.π φ₁ φ₂)) ⋯
rw :
  Eq (α := G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
    (φ₁ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a)) (φ₂ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a))
⊢ Eq (α := G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
    (φ₁ ≫ colimit.ι Φ j) (φ₂ ≫ colimit.ι Φ j)

Tactic:
rw [← colimit.w Φ ψ]

Premises used: CategoryTheory.Limits.colimit.w
-- 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_2 : 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)))
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory :=
  FullSubcategory.mk (P := P.colimitsCardinalClosure κ) (coequalizer φ₁ φ₂) ⋯
a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X := coequalizer.desc ((E.coconeAt X).ι.app j) ⋯
ψ : j ⟶ CostructuredArrow.mk a :=
  CostructuredArrow.homMk (homMk (P := P.colimitsCardinalClosure κ) (coequalizer.π φ₁ φ₂)) ⋯
⊢ Eq (α := G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
    (φ₁ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a)) (φ₂ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a))

Tactic:
apply coequalizer.condition_assoc

Premises used: CategoryTheory.Limits.coequalizer.condition_assoc
-- 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
⊢ 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:
have : Mono (colimit.desc _ (E.coconeAt X)) := by
      let Φ := CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙
        (P.colimitsCardinalClosure κ).ι
      rw [hS₁.isSeparating.mono_iff]
      intro G hG (g₁ : G ⟶ colimit Φ) (g₂ : G ⟶ colimit Φ)
        (h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X))
      have : IsCardinalPresentable G κ := hS₂ _ hG
      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⟩
      have : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair := by
        apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure
        refine .of_le ?_ (Cardinal.IsRegular.aleph0_le Fact.out)
        simp only [hasCardinalLT_aleph0_iff]
        infer_instance
      let obj : (P.colimitsCardinalClosure κ).FullSubcategory :=
        ⟨coequalizer φ₁ φ₂, by
          apply ObjectProperty.prop_colimit
          rintro (_ | _)
          · exact P.le_colimitsCardinalClosure _ _ hG
          · exact j.left.2⟩
      let a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X :=
        coequalizer.desc ((E.coconeAt X).ι.app j) (by simpa using h)
      let ψ : j ⟶ CostructuredArrow.mk a :=
        CostructuredArrow.homMk (ObjectProperty.homMk (coequalizer.π _ _)) (by simp [E, a])
      rw [← colimit.w Φ ψ]
      apply coequalizer.condition_assoc
-- 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
this :
  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))
Y : C
hY : P Y
g : Y ⟶ (E.coconeAt X).pt
⊢ (P.colimitsCardinalClosure κ).ι.obj (FullSubcategory.mk (P := P.colimitsCardinalClosure κ) Y ⋯) ⟶ X

Tactic:
exact g
-- 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
this :
  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))
Y : C
hY : P Y
g : Y ⟶ (E.coconeAt X).pt
γ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X :=
  CostructuredArrow.mk (Y := FullSubcategory.mk (P := P.colimitsCardinalClosure κ) Y ⋯) g
⊢ (fun (f : Y ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)) ↦
        (f ≫
            colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
              (E.coconeAt X) :
          Y ⟶ (E.coconeAt X).pt))
      (colimit.ι (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι) γ) =
    g

Tactic:
simp [γ, E]
-- 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
this :
  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))
Y : C
hY : P Y
g : Y ⟶ (E.coconeAt X).pt
γ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X :=
  CostructuredArrow.mk (Y := FullSubcategory.mk (P := P.colimitsCardinalClosure κ) Y ⋯) g
⊢ ∃ (a : Y ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
    (fun
            (f :
              Y ⟶
                colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)) ↦
          (f ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) :
            Y ⟶ (E.coconeAt X).pt))
        a =
      g

Tactic:
exact ⟨colimit.ι (CostructuredArrow.proj _ _ ⋙ (P.colimitsCardinalClosure κ).ι) γ,
        by simp [γ, E]⟩
-- 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
this :
  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))
⊢ IsIso (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:
have : IsIso (colimit.desc _ (E.coconeAt X)) := hS₁.isIso_of_mono _ (fun Y hY g ↦ by
      let γ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X :=
        CostructuredArrow.mk (Y := ⟨Y, P.le_colimitsCardinalClosure  _ _ hY⟩) (by exact g)
      exact ⟨colimit.ι (CostructuredArrow.proj _ _ ⋙ (P.colimitsCardinalClosure κ).ι) γ,
        by simp [γ, E]⟩)