awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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) κ
⊢ P.IsCardinalFilteredGenerator κ
have rw : P.isoClosure.IsCardinalFilteredGenerator κ
Tactic: rw [← ObjectProperty.IsCardinalFilteredGenerator.isoClosure_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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) κ
⊢ P.isoClosure.IsCardinalFilteredGenerator κ
have this : ∀ (X : P.FullSubcategory), IsCardinalPresentable.{w, v, u} (P.ι.obj X) κ
Tactic: have (X : P.FullSubcategory) : IsCardinalPresentable (P.ι.obj X) κ := hP _ X.property
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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) κ
⊢ Cocone K
have this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J
Tactic: have := ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure P κ J hJ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X
have this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Tactic: have : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C :=
      hasColimitsOfShape_of_equivalence
        (equivSmallModel.{w} (CostructuredArrow (P.colimitsCardinalClosure κ).ι X)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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 κ).ι
⊢ 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))
have 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₂
Tactic: rw [hS₁.isSeparating.mono_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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))
⊢ g₁ = g₂
have this₁ : IsCardinalPresentable.{w, v, u} G κ
Tactic: have : IsCardinalPresentable G κ := hS₂ _ hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
    φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂
have 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₂
Tactic: obtain ⟨j₁, f₁, hf₁⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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) (φ₁ : G ⟶ Φ.obj j) (φ₂ : G ⟶ Φ.obj j),
    φ₁ ≫ colimit.ι Φ j = g₁ ∧ φ₂ ≫ colimit.ι Φ j = g₂
have 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₂
Tactic: obtain ⟨j₂, f₂, hf₂⟩ :=
          IsCardinalPresentable.exists_hom_of_isColimit κ (colimit.isColimit _) g₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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 κ
⊢ g₁ = g₂
have 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)
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⟩
Cleared hypotheses: g₁, g₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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
have hJ : HasCardinalLT (Arrow WalkingParallelPair) κ
Tactic: apply ObjectProperty.isClosedUnderColimitsOfShape_colimitsCardinalClosure
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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) κ
have hJ : HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0
Tactic: refine .of_le ?_ (Cardinal.IsRegular.aleph0_le Fact.out)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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) Cardinal.aleph0
have hJ : Finite (Arrow WalkingParallelPair)
Tactic: simp only [hasCardinalLT_aleph0_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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)))
⊢ Eq (α := G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
    (φ₁ ≫ colimit.ι Φ j) (φ₂ ≫ colimit.ι Φ j)
have this₁ : (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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 κ (coequalizer φ₁ φ₂)
have hF : ∀ (j_1 : WalkingParallelPair), P.colimitsCardinalClosure κ ((parallelPair φ₁ φ₂).obj j_1)
Tactic: apply ObjectProperty.prop_colimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (goal)
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 κ).ι))
    (φ₁ ≫ colimit.ι Φ j) (φ₂ ≫ colimit.ι Φ j)
have rw : Eq (α := G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
  (φ₁ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a)) (φ₂ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a))
Tactic: rw [← colimit.w Φ ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X
have 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))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.StrongGenerator (hypothesis)
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))
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X
have this₁ : 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]⟩)