awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₁ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₂ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
⊢ ∃ (j' : J) (α : j ⟶ j'),
    Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map α)) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) → (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
          x₁ :
        (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map α)) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) → (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
          x₂ :
        (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₁ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₂ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
this : IsFiltered J
y₁ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₁
y₂ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₂
⊢ ∃ (j' : J) (α : j ⟶ j'),
    Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map α)) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) → (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
          x₁ :
        (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map α)) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) → (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
          x₂ :
        (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
have hy₁ : (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
      (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
        (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
    y₁ =
  x₁
Tactic: have hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁ := by simp [y₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h :
  Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₁ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (cX.ι.app j)) :
          (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) →
            (fun (X : Type w') ↦ X) (c.pt.obj (((const J).obj cX.pt).obj j)))
        x₂ :
      (fun (X : Type w') ↦ X) (c.pt.obj (obj.{w, v, w, u} (obj (const J) cX.pt) j)))
this : IsFiltered J
y₁ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₁
y₂ : (↑(F ⋙ obj (evaluation C (Type w')) (X.obj j)).sections : Type (max w' u')) :=
  (Types.isLimitEquivSections (hc (X.obj j)) :
      (a : (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt) →
        (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u')))
    x₂
hy₁ :
  (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
      y₁ =
    x₁
⊢ ∃ (j' : J) (α : j ⟶ j'),
    Eq (α := (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map α)) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) → (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
          x₁ :
        (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.pt.map (X.map α)) :
            (a : (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j))) → (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
          x₂ :
        (fun (X : Type w') ↦ X) (c.pt.obj (X.obj j')))
have hy₂ : (Equiv.symm (Types.isLimitEquivSections (hc (X.obj j))) :
      (a : (↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections : Type (max w' u'))) →
        (((evaluation C (Type w')).obj (X.obj j)).mapCone c).pt)
    y₂ =
  x₂
Tactic: have hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂ := by simp [y₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
⊢ IsColimit (c.pt.mapCocone cX)
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ IsColimit (c.pt.mapCocone cX)
have hsurj : ∀ (x : (c.pt.mapCocone cX).pt),
  ∃ (i : J) (xi : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
            (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
        xi
Tactic: apply Types.FilteredColimit.isColimitOf'
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
hsurj :
  ∀ (x : (c.pt.mapCocone cX).pt),
    ∃ (i : J) (xi : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
            (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
              (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
          xi
⊢ IsColimit (c.pt.mapCocone cX)
have hinj : ∀ (i : J) (x y : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)),
  Eq (α := (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
            (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
              (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
          x :
        (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app i) :
            (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) →
              (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj i))
          y :
        (fun (X : Type w') ↦ X) (obj (obj (const J) (c.pt.mapCocone cX).pt) i)) →
    ∃ (k : J) (f : i ⟶ k),
      Eq (α := (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
            x :
          (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X ⋙ c.pt).map f) :
              (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj i)) → (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
            y :
          (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj k))
Tactic: apply Types.FilteredColimit.isColimitOf'
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : IsLimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', w', w' + 1} K (Type w')
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), (F.obj k).IsCardinalAccessible κ
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hcX : IsColimit cX
⊢ Nonempty (IsColimit (c.pt.mapCocone cX))
have this : ∀ (k : K), PreservesColimitsOfShape J (F.obj k)
Tactic: have := fun k ↦ preservesColimitsOfShape_of_isCardinalAccessible (F.obj k) κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
k : Kᵒᵖ
⊢ ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
have dsimp : Functor.IsCardinalAccessible.{w, v, v, u, v + 1} (Functor.obj coyoneda (op (Y.obj (unop k)))) κ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasLimitsOfShape.{v', u', v, v + 1} Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_4 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
⊢ IsCardinalPresentable.{w, v, u} c.pt κ
have this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
Tactic: have (k : Kᵒᵖ) : ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ := by
    dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
k : K
⊢ IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
have dsimp : IsCardinalPresentable (e.functor.obj (Y.obj k)) κ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
⊢ IsCardinalPresentable.{w, v, u} c.pt κ
have this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
Tactic: have (k : K) : IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ := by
    dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
⊢ IsCardinalPresentable.{w, v, u} c.pt κ
have rw : IsCardinalPresentable (e.functor.obj c.pt) κ
Tactic: rw [← isCardinalPresentable_iff_of_isEquivalence c.pt κ e.functor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', w, w + 1} Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
X : C
hX : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
⊢ isCardinalPresentable.{w, v, u} C κ X
have this : ∀ (j : J), isCardinalPresentable.{w, v, u} C κ (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j)
Tactic: have := hX.prop_diag_obj
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', w, w + 1} Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
X : C
hX : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this :
  ∀ (j : J), isCardinalPresentable.{w, v, u} C κ (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j)
⊢ isCardinalPresentable.{w, v, u} C κ X
have this₁ : ∀ (j : J), IsCardinalPresentable.{w, v, u} (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j) κ
Tactic: simp only [isCardinalPresentable_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.LocallyPresentable (goal)
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsLocallyPresentable.{w, v, u} C
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ
have obtain : ∀ (κ : Cardinal.{w}) (hκ : Fact κ.IsRegular) (h' : IsCardinalLocallyPresentable.{w, v, u} C κ),
  ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ
Tactic: obtain ⟨κ, hκ, h'⟩ := IsLocallyPresentable.exists_cardinal C
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.LocallyPresentable (goal)
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsAccessibleCategory.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X
have obtain : ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ → IsPresentable.{w, v, u} X
Tactic: obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.LocallyPresentable (goal)
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalAccessibleCategory.{w, v, u} C κ
⊢ IsPresentable.{w, v, u} X
have obtain : ∀ (w_1 : ObjectProperty.{v, u} C),
  ObjectProperty.EssentiallySmall.{w, v, u} w_1 → ∀ (h : w_1.IsCardinalFilteredGenerator κ), IsPresentable.{w, v, u} X
Tactic: obtain ⟨_, _, h⟩ := HasCardinalFilteredGenerator.exists_generator C κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have left : IsCardinalPresentable.{w, v, u} X κ
Tactic: obtain ⟨_, _⟩ := hW f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have right : IsCardinalPresentable.{w, v, u} Y κ
Tactic: obtain ⟨_, _⟩ := hW f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have refine_1 : ∀ (g₁ g₂ : Y ⟶ Z) (h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)), g₁ = g₂
Tactic: refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
refine_1 :
  ∀ (g₁ g₂ : Y ⟶ Z) (h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)), g₁ = g₂
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have refine_2 : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
Tactic: refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
g₁ g₂ : Y ⟶ Z
h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
⊢ g₁ = g₂
have refine_1 : ∀ (j₁ : J) (g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁)
  (h :
    Eq.{v + 1} (α := X ⟶ Z)
      ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₁))
      ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)),
  g₁ ≫
      { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
              Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
        j₁ =
    g₂
Tactic: obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₁
Cleared hypotheses: g₁, h