awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered J κ
this : IsFiltered.{w, w} κ.ord.ToType
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final
have obtain : ∀ (α : Type w) (w : PartialOrder α),
  IsCardinalFiltered α κ →
    ∀ (F : α ⥤ J × κ.ord.ToType),
      F.Final → ∃ (α : Type w) (x : PartialOrder α) (_ : IsCardinalFiltered α κ) (F : α ⥤ J), F.Final
Tactic: obtain ⟨α, _, _, F, _⟩ :=
    exists_cardinal_directed.aux (J × κ.ord.ToType) κ (fun ⟨j, x⟩ ↦
      ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
        have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J), F.Final
have this : IsCardinalFiltered J Cardinal.aleph0
Tactic: have := (isCardinalFiltered_aleph0_iff.{w} J).2 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (goal)
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J), F.Final
have obtain : ∀ (α : Type w) (w : PartialOrder α),
  IsCardinalFiltered α Cardinal.aleph0 →
    ∀ (F : α ⥤ J),
      F.Final →
        ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J),
          F.Final
Tactic: obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J .aleph0
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Directed (hypothesis)
Goal:
J : Type w
inst : SmallCategory J
inst_1 : IsFiltered J
this : IsCardinalFiltered J Cardinal.aleph0
α : Type w
w : PartialOrder α
w_1 : IsCardinalFiltered α Cardinal.aleph0
F : α ⥤ J
h : F.Final
⊢ ∃ (α : Type w) (x : PartialOrder α) (_ : IsDirected α fun (x1 x2 : α) ↦ x1 ≤ x2) (_ : Nonempty α) (F : α ⥤ J), F.Final
have this₁ : IsFiltered α
Tactic: have : IsFiltered α := by rwa [← isCardinalFiltered_aleph0_iff.{w}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.EssentiallyLarge (goal)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤
have refine : ∀ (X : C), ⊤ X → ObjectProperty.isoClosure.{v, u} (ofObj φ) X
Tactic: refine ⟨ObjectProperty.ofObj φ, inferInstance, fun X _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.EssentiallyLarge (goal)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
⊢ ObjectProperty.isoClosure.{v, u} (ofObj φ) X
have obtain : ∀ (J : Type w) (w : SmallCategory J),
  IsCardinalFiltered J κ → ∀ (p : P.ColimitOfShape J X), ObjectProperty.isoClosure.{v, u} (ofObj φ) X
Tactic: obtain ⟨J, _, _, ⟨p⟩⟩ := hP.exists_colimitsOfShape X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.EssentiallyLarge (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : Functor.{w, v, w, u} J P.FullSubcategory := P.lift p.toColimitPresentation (P := P).diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.toColimitPresentation (P := P).diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
⊢ ObjectProperty.isoClosure.{v, u} (ofObj φ) X
have this : HasColimit p.toColimitPresentation (P := P).diag
Tactic: have : HasColimit p.diag := ⟨_, p.isColimit⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.EssentiallyLarge (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_3 : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : Equivalence.{v, w, u, w} P.FullSubcategory (SmallModel.{w, v, u} P.FullSubcategory) :=
  equivSmallModel P.FullSubcategory
ι : Type (w + 1) :=
  (J : Type w) ×
    (x : SmallCategory J) × { F : J ⥤ SmallModel.{w, v, u} P.FullSubcategory // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
φ : ι → C :=
  fun (x : ι) ↦
    match (motive := ι → C) x with
    | ⟨j, ⟨fst, ⟨F, hF⟩⟩⟩ => colimit (F ⋙ e.inverse ⋙ P.ι)
X : C
h : ⊤ X
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
G : Functor.{w, v, w, u} J P.FullSubcategory := P.lift p.toColimitPresentation (P := P).diag ⋯
iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.toColimitPresentation (P := P).diag :=
  G.associator e.functor (e.inverse ⋙ P.ι) ≪≫
    G.isoWhiskerLeft ((e.functor.associator e.inverse P.ι).symm ≪≫ Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
      (G.associator (𝟭 P.FullSubcategory) P.ι).symm ≪≫ Functor.isoWhiskerRight G.rightUnitor P.ι
this : HasColimit p.toColimitPresentation (P := P).diag
⊢ ObjectProperty.isoClosure.{v, u} (ofObj φ) X
have this₁ : HasColimit ((G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι)
Tactic: have := hasColimit_of_iso iso
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.EssentiallyLarge (goal)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
⊢ ∃ (J : Type (w + 1)) (x : Category.{w, w + 1} J), Nonempty (Equivalence.{v, w, u, w + 1} C J)
have rw : ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤
Tactic: rw [exists_equivalence_iff_of_locallySmall]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.EssentiallyLarge (goal)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤
have obtain : ∀ (P : ObjectProperty.{v, u} C),
  ObjectProperty.EssentiallySmall.{w, v, u} P →
    ∀ (hP : P.IsCardinalFilteredGenerator κ), ObjectProperty.EssentiallySmall.{w + 1, v, u} (C := C) ⊤
Tactic: obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
have refine_1 : F.IsFinitelyAccessible →
  ∀ (H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F) (J : Type w)
    [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
Tactic: refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
refine_1 :
  F.IsFinitelyAccessible →
    ∀ (H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F)
      (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ F.IsFinitelyAccessible ↔ PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
have refine_2 : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F →
  ∀ (H : ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F) (J : Type w)
    [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
Tactic: refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
have H₁ : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
Tactic: simp only [isCardinalFiltered_aleph0_iff] at *
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
h : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst_2 : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst_2 : SmallCategory J] [IsCardinalFiltered J ℵ₀], PreservesColimitsOfShape J F
have refine_2 : ∀ (J : Type w) [inst_2 : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
Tactic: simp only [isCardinalFiltered_aleph0_iff] at *
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
have this : Nonempty J
Tactic: have : Nonempty J := IsFiltered.nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
have obtain : ∀ (j : J) (q : Under.mk p ⟶ (Under.lift D s).obj j)
  (hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f sorry),
  ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
Tactic: obtain ⟨j, q, hq⟩ := exists_hom_of_isColimit (X := Under.mk p) hc' (Under.homMk f rfl)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
j : J
q : Under.mk p ⟶ (Under.lift D s).obj j
hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f ⋯
w : J
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
have w₁ : A ⟶ D.obj j
Tactic: use j, q.right, Under.w q, congr($(hq).right)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
j : J
q : Under.mk p ⟶ (Under.lift D s).obj j
hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f ⋯
w : J
w₁ : A ⟶ D.obj j
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
have left : p ≫ Under.Hom.right q = s.app j
Tactic: use j, q.right, Under.w q, congr($(hq).right)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
j : J
q : Under.mk p ⟶ (Under.lift D s).obj j
hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f ⋯
w : J
w₁ : A ⟶ D.obj j
left : p ≫ Under.Hom.right q = s.app j
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
have right : Under.Hom.right q ≫ c.ι.app j = f
Tactic: use j, q.right, Under.w q, congr($(hq).right)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ HasCardinalFilteredColimits.{w, v, u} C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C
have refine_1 : HasCardinalFilteredColimits.{w, v, u} C ℵ₀ →
  ∀ (H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C)
    (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
Tactic: refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
refine_1 :
  HasCardinalFilteredColimits.{w, v, u} C ℵ₀ →
    ∀ (H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C)
      (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
⊢ HasCardinalFilteredColimits.{w, v, u} C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C
have refine_2 : HasFilteredColimitsOfSize.{w, w, v, u} C →
  ∀ (H : ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C) (J : Type w)
    [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C
Tactic: refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : HasCardinalFilteredColimits.{w, v, u} C ℵ₀
H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C
⊢ ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
have H₁ : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C
Tactic: simp only [isCardinalFiltered_aleph0_iff] at *
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Finite (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
⊢ ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C
have refine_2 : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C
Tactic: simp only [isCardinalFiltered_aleph0_iff] at *
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
⊢ Cocone F
have this : Small.{w, max u' v'} (Arrow.{u', v'} A)
Tactic: have := hA.small
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
this : Small.{w, max u' v'} (Arrow.{u', v'} A)
⊢ Cocone F
have this₁ : Small.{w, v'} A
Tactic: have := small_of_small_arrow.{w} A
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
this_1 : Small.{w, max u' v'} (Arrow.{u', v'} A)
this : Small.{w, v'} A
⊢ Cocone F
have this₁ : LocallySmall.{w, u', v'} A
Tactic: have := locallySmall_of_small_arrow.{w} A
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
⊢ IsFiltered.{v, u} J
have rw : ∀ {J_1 : Type w} [inst_2 : SmallCategory J_1] [FinCategory J_1] (F : Functor.{w, v, w, u} J_1 J), Nonempty (Cocone F)
Tactic: rw [IsFiltered.iff_cocone_nonempty.{w}]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
⊢ HasCardinalLT (Arrow A) κ
have refine : HasCardinalLT (Arrow A) Cardinal.aleph0
Tactic: refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
⊢ HasCardinalLT (Arrow A) Cardinal.aleph0
have simp : Finite.{w + 1} (Arrow A)
Tactic: simp only [hasCardinalLT_aleph0_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
⊢ Nonempty (Cocone F)
have hA : HasCardinalLT (Arrow A) κ
Tactic: have hA : HasCardinalLT (Arrow A) κ := by
    refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
    simp only [hasCardinalLT_aleph0_iff]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
⊢ IsCardinalFiltered.{w, v, u} J Cardinal.aleph0 ↔ IsFiltered.{v, u} J
have mp : IsCardinalFiltered.{w, v, u} J Cardinal.aleph0 → IsFiltered.{v, u} J
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
mp : IsCardinalFiltered.{w, v, u} J Cardinal.aleph0 → IsFiltered.{v, u} J
⊢ IsCardinalFiltered.{w, v, u} J Cardinal.aleph0 ↔ IsFiltered.{v, u} J
have mpr : IsFiltered.{v, u} J → IsCardinalFiltered.{w, v, u} J Cardinal.aleph0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
⊢ IsCardinalFiltered.{w, v, u} J Cardinal.aleph0
have mpr : ∀ {A : Type w} [inst_1 : SmallCategory A] (F : Functor.{w, v, w, u} A J) (hA : HasCardinalLT (Arrow A) Cardinal.aleph0),
  Nonempty (Cocone F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
inst_1 : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) Cardinal.aleph0
⊢ Nonempty (Cocone F)
have hA₁ : Finite.{w + 1} (Arrow A)
Tactic: rw [hasCardinalLT_aleph0_iff] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
inst_1 : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : Finite.{w + 1} (Arrow A)
⊢ Nonempty (Cocone F)
have mpr : ∀ (this : FinCategory A), Nonempty (Cocone F)
Tactic: have := ((Arrow.finite_iff A).1 hA).some
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
J : Type w
inst : Preorder J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ (j : J), ∀ (k : K), s k ≤ j
A : Type w
x : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty.{w + 1} (Cocone F)
have obtain : ∀ (j : J) (hj : ∀ (k : A), F.obj k ≤ j), Nonempty.{w + 1} (Cocone F)
Tactic: obtain ⟨j, hj⟩ := h F.obj (by simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
        hasCardinalLT_of_hasCardinalLT_arrow hA)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
⊢ ∃ (j : κ.ord.ToType), ∀ (k : ι), f k ≤ j
have h : Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
  Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) sorry
Tactic: have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := fun _ ↦ by aesop
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
⊢ ∃ (j : κ.ord.ToType), ∀ (k : ι), f k ≤ j
have contrapose! : ∀ (hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k), κ ≤ Cardinal.mk ι
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
⊢ κ ≤ Cardinal.mk ι
have rw : Order.cof κ.ord.ToType ≤ Cardinal.mk ι
Tactic: rw [← hκ.out.cof_ord, ← Ordinal.cof_toType]