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
κ : 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 κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ
have refine : isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ
Tactic: refine le_antisymm ?_ (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)
-- 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 κ
⊢ isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ
have this : (P.colimitsCardinalClosure κ).ι.IsDense
Tactic: have := hS₁.isDense_colimitsCardinalClosure_ι hS₂
-- 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 κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : isCardinalPresentable.{w, v, u} C κ X
⊢ P.colimitsCardinalClosure κ X
have hX₁ : IsCardinalPresentable.{w, v, u} X κ
Tactic: rw [isCardinalPresentable_iff] at hX
Cleared hypotheses: hX
-- 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 κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
⊢ P.colimitsCardinalClosure κ X
have rw : (P.colimitsCardinalClosure κ).retractClosure X
Tactic: rw [← (P.colimitsCardinalClosure κ).retractClosure_eq_self]
-- 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 κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
⊢ (P.colimitsCardinalClosure κ).retractClosure X
have obtain : ∀ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X)
  (φ : X ⟶ (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι).obj j)
  (hφ :
    φ ≫ ((Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv).coconeAt X).ι.app j = 𝟙 X),
  (P.colimitsCardinalClosure κ).retractClosure X
Tactic: obtain ⟨j, φ, hφ⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ
    ((P.colimitsCardinalClosure κ).ι.denseAt X) (𝟙 X)
-- 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
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ ↔
    ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
have refine_1 : IsCardinalLocallyPresentable.{w, v, u} C κ →
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
Tactic: refine ⟨fun _ ↦ ?_, fun ⟨P, _, hS₁, hS₂⟩ ↦ ?_⟩
-- 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
refine_1 :
  IsCardinalLocallyPresentable.{w, v, u} C κ →
    ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ ↔
    ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
have refine_2 : (∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ) →
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} P →
      ∀ (hS₁ : P.IsStrongGenerator) (hS₂ : P ≤ isCardinalPresentable C κ), IsCardinalLocallyPresentable.{w, v, u} C κ
Tactic: refine ⟨fun _ ↦ ?_, fun ⟨P, _, hS₁, hS₂⟩ ↦ ?_⟩
-- 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
h : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
have refine_1 : ∀ (P : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} P →
    ∀ (hP : P.IsCardinalFilteredGenerator κ),
      ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
        P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
Tactic: obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_small_generator C κ
-- 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
h :
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ
have this : (P.colimitsCardinalClosure κ).ι.IsDense
Tactic: have := hS₁.isDense_colimitsCardinalClosure_ι hS₂
-- 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
h :
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ
have this₁ : HasCardinalFilteredGenerator.{w, v, u} C κ
Tactic: have : HasCardinalFilteredGenerator C κ :=
      { exists_generator := ⟨(P.colimitsCardinalClosure κ), inferInstance,
            IsCardinalFilteredGenerator.of_isDense_ι _ _
              (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)⟩ }
-- 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 : IsCardinalLocallyPresentable.{w, v, u} C κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ'
have rw : ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
  P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
Tactic: rw [iff_exists_isStrongGenerator]
-- 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 : IsCardinalLocallyPresentable.{w, v, u} C κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
have obtain : ∀ (S : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} S →
    ∀ (h₁ : S.IsStrongGenerator) (h₂ : S ≤ isCardinalPresentable C κ),
      ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
        P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
Tactic: obtain ⟨S, _, h₁, h₂⟩ := (iff_exists_isStrongGenerator C κ).1 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)
have refine_1 : ∀ (f : Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)),
  ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi
Tactic: refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
refine_1 :
  ∀ (f : Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
      f =
        (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
          xi
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)
have refine_2 : ∀ (j : J) (f g : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj j))
  (h :
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
          j))
      ((hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) j) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj j))
          f :
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
            j))
      ((hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) j) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj j))
          g :
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
            j))),
  ∃ (k : J) (f_1 : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
      ((hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (op X)).map f_1) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj k))
          f :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
      ((hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (op X)).map f_1) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj k))
          g :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
Tactic: refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi
have refine_1 : ∀ (j : (x : X) → J) (g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1)))
  (hg :
    ∀ (x_1 : X),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
        ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
              (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
            (g x_1) :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
        ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
          (fun (X : Type u) ↦ X) c.pt)),
  ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi
Tactic: choose j g hg using fun x ↦ Types.jointly_surjective_of_isColimit hc (f x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi
have refine_1 : f =
  (hom (FC := TypeCat.Fun)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) (IsCardinalFiltered.max j hX)) :
      (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj (IsCardinalFiltered.max j hX))) →
        (fun (X : Type u) ↦ X)
          (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj (IsCardinalFiltered.max j hX)))
    (↾fun (x_1 : unop (op X)) ↦
      (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
          (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) → (fun (X : Type u) ↦ X) (F.obj (IsCardinalFiltered.max j hX)))
        (g x_1))
Tactic: refine ⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
⊢ f =
    (hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) (IsCardinalFiltered.max j hX)) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj (IsCardinalFiltered.max j hX))) →
          (fun (X : Type u) ↦ X)
            (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj (IsCardinalFiltered.max j hX)))
      (↾fun (x_1 : unop (op X)) ↦
        (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) → (fun (X : Type u) ↦ X) (F.obj (IsCardinalFiltered.max j hX)))
          (g x_1))
have refine_1 : f =
  CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
    (↾fun (x_1 : X) ↦
      (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
          (a : F.obj (j x_1)) → F.obj (IsCardinalFiltered.max j hX))
        (g x_1))
    (c.ι.app (IsCardinalFiltered.max j hX))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
⊢ f =
    CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
      (↾fun (x_1 : X) ↦
        (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
            (a : F.obj (j x_1)) → F.obj (IsCardinalFiltered.max j hX))
          (g x_1))
      (c.ι.app (IsCardinalFiltered.max j hX))
have refine_1 : ∀ (x_1 : X),
  (hom (FC := TypeCat.Fun) f).toFun x_1 =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
          (↾fun (x_2 : X) ↦
            (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_2)) :
                (a : F.obj (j x_2)) → F.obj (IsCardinalFiltered.max j hX))
              (g x_2))
          (c.ι.app (IsCardinalFiltered.max j hX))))
      x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x : X) → (fun (X : Type u) ↦ X) (F.obj (j x))
hg :
  ∀ (x : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x)))
          (g x) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x :
        (fun (X : Type u) ↦ X) c.pt)
x : X
⊢ (hom (FC := TypeCat.Fun) f).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
          (↾fun (x : X) ↦
            (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
                (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
              (g x))
          (c.ι.app (IsCardinalFiltered.max j hX))))
      x
have refine_1 : Eq (α := c.pt) ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
  ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) : (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
      ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
            (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
          (g x) :
        F.obj (IsCardinalFiltered.max j hX)) :
    c.pt)
Tactic: dsimp at j g hg x ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x : X) → F.obj (j x)
hg :
  ∀ (x : X),
    Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
      ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
x : X
⊢ Eq (α := c.pt) ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
    ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) :
          (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
        ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
              (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
            (g x) :
          F.obj (IsCardinalFiltered.max j hX)) :
      c.pt)
have refine_1 : Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
  ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) : (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
      ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
            (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
          (g x) :
        F.obj (IsCardinalFiltered.max j hX)) :
    c.pt)
Tactic: rw [← hg]