awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)))
have this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
Tactic: have := preservesColimitsOfShape_of_isCardinalPresentable X κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)))
have suffices : PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
Tactic: suffices PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) from
    ⟨fun {c} hc ↦ ⟨isColimitOfReflects uliftFunctor.{v₁}
        (isColimitOfPreserves (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) hc)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
X_1 Y_1 : C'
f : X_1 ⟶ Y_1
⊢ Eq (α :=
    Functor.obj (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) X_1 ⟶
      (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).obj Y_1)
    (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
      Iso.hom
        ((fun (Z : C') ↦ (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
          Y_1))
    (Iso.hom
        ((fun (Z : C') ↦ (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
          X_1) ≫
      (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)
have h : ∀ (g : Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
          Iso.hom
            ((fun (Z : C') ↦
                (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
              Y_1)))
      { down := g : ULift.{v₁, v₃} (Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Z : C') ↦
                (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
              X_1) ≫
          (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f))
      { down := g : ULift.{v₁, v₃} (Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1) }
Tactic: ext ⟨g⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
have have : ∀
  (iso :
    Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅
      e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}),
  PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
Tactic: have iso : coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁} ≅
    e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃} :=
    NatIso.ofComponents (fun Z ↦
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) (by
        intro _ _ f
        ext ⟨g⟩
        simp [Adjunction.homEquiv_unit])
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_3 : F.IsEquivalence
⊢ IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ ↔ IsCardinalPresentable.{w, v₁, u₁} X κ
have mp : IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ → IsCardinalPresentable.{w, v₁, u₁} X κ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_3 : F.IsEquivalence
mp : IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ → IsCardinalPresentable.{w, v₁, u₁} X κ
⊢ IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ ↔ IsCardinalPresentable.{w, v₁, u₁} X κ
have mpr : IsCardinalPresentable.{w, v₁, u₁} X κ → IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
f : X ⟶ c.pt
⊢ ∃ (j : J) (f' : X ⟶ F.obj j), f' ≫ c.ι.app j = f
have this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
Tactic: have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
⊢ ∃ (j : J) (u : i₁ ⟶ j) (v : i₂ ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map v
have this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
Tactic: have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ ∃ (j : J) (u : i₁ ⟶ j) (v : i₂ ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map v
have this₁ : IsFiltered.{v₂, u₂} J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
⊢ ∃ (j : J) (u : i ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map u
have this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
Tactic: have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ ∃ (j : J) (u : i ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map u
have this₁ : IsFiltered.{v₂, u₂} J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ ↔ Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{t, v₁, u₁} (op X)) κ
have change : IsCardinalPresentable.{w, v₁, u₁} X κ ↔
  Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
Tactic: change _ ↔ (coyoneda.obj (op X) ⋙ uliftFunctor.{t}).IsCardinalAccessible κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ ↔
    Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
have refine : Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ →
  ∀ (J : Type w) (x : SmallCategory J),
    IsCardinalFiltered J κ → PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
Tactic: refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun J _ _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : Functor.IsCardinalAccessible (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁}) κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
have this : PreservesColimitsOfShape J (Functor.obj coyoneda (op X) ⋙ uliftFunctor.{t, v₁})
Tactic: have := Functor.preservesColimitsOfShape_of_isCardinalAccessible
    (coyoneda.obj (op X) ⋙ uliftFunctor.{t}) κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
P' : ObjectProperty.{v, u} C
h₁ : P ≤ P'.isoClosure
h₂ : P' ≤ isCardinalPresentable C κ
X : C
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X
have obtain : ∀ (J : Type w) (w : SmallCategory J),
  IsCardinalFiltered J κ →
    ∀ (hX : P.colimitsOfShape J X),
      ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X
Tactic: obtain ⟨J, _, _, hX⟩ := h.exists_colimitsOfShape X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X
have obtain : ∀ (J : Type w) (w : SmallCategory J), IsCardinalFiltered J κ → ∀ (hX : P.ColimitOfShape J X), IsPresentable.{w, v, u} X
Tactic: obtain ⟨J, _, _, ⟨hX⟩⟩ := h.exists_colimitsOfShape X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
⊢ ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'
have obtain : ∀ (κ' : Cardinal.{w}) (h₁ : κ'.IsRegular)
  (h₂ : ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun (x : Unit) ↦ Arrow J) (fun (x : Unit) ↦ κ.ord.ToType) i) κ'),
  ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'
Tactic: obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.ToType))
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
⊢ IsPresentable.{w, v, u} X
have obtain : ∀ (κ' : Cardinal.{w}), Fact κ'.IsRegular → ∀ (le : κ ≤ κ') (hκ' : HasCardinalLT (Arrow J) κ'), IsPresentable.{w, v, u} X
Tactic: obtain ⟨κ', _, le, hκ'⟩ : ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'),
      HasCardinalLT (Arrow J) κ' := by
    obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.ToType))
    exact ⟨κ', ⟨h₁⟩,
      le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)),
      h₂ (Sum.inl ⟨⟩)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : LocallySmall.{w, v, u} C
X : C
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
w_2 : Fact κ'.IsRegular
le : κ ≤ κ'
hκ' : HasCardinalLT (Arrow J) κ'
⊢ IsPresentable.{w, v, u} X
have this : IsCardinalPresentable.{w, v, u} X κ'
Tactic: have := hX.isCardinalPresentable h.le_isCardinalPresentable _ le hκ'
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
⊢ ∃ (J : Type w) (x : Category.{w, w} J), P.colimitsOfShape J X
have obtain : ∀ (w : Type w) (w_1 : SmallCategory w),
  IsCardinalFiltered w κ → ∀ (hX : P.colimitsOfShape w X), ∃ (J : Type w) (x : Category.{w, w} J), P.colimitsOfShape J X
Tactic: obtain ⟨_, _, _, hX⟩ := h.exists_colimitsOfShape X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ isCardinalPresentable C κ = P.retractClosure
have refine_1 : ∀ (X : C) (hX : isCardinalPresentable.{w, v, u} C κ X), P.retractClosure X
Tactic: refine le_antisymm (fun X hX ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
refine_1 : ∀ (X : C) (hX : isCardinalPresentable.{w, v, u} C κ X), P.retractClosure X
⊢ isCardinalPresentable C κ = P.retractClosure
have refine_2 : P.retractClosure ≤ isCardinalPresentable C κ
Tactic: refine le_antisymm (fun X hX ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : isCardinalPresentable.{w, v, u} C κ X
⊢ P.retractClosure 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.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
⊢ P.retractClosure X
have refine_1 : ∀ (J : Type w) (w : SmallCategory J), IsCardinalFiltered J κ → ∀ (p : P.ColimitOfShape J X), P.retractClosure X
Tactic: obtain ⟨J, _, _, ⟨p⟩⟩ := h.exists_colimitsOfShape X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
⊢ P.retractClosure X
have this : EssentiallySmall.{w, w, w} J
Tactic: have := essentiallySmall_of_small_of_locallySmall.{w} J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
⊢ P.retractClosure X
have refine_1 : ∀ (j : J) (f : X ⟶ p.toColimitPresentation (P := P).diag.obj j)
  (hf :
    f ≫ { pt := X, ι := p.toColimitPresentation (P := P).ι : Cocone p.toColimitPresentation (P := P).diag }.ι.app j =
      𝟙 X),
  P.retractClosure X
Tactic: obtain ⟨j, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit (𝟙 X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst_2 : ObjectProperty.EssentiallySmall.{w, v, u} P
inst_3 : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)
have rw : ObjectProperty.EssentiallySmall.{w, v, u} P.retractClosure
Tactic: rw [h.isPresentable_eq_retractClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
have obtain : ∀ (P : ObjectProperty.{v, u} C),
  ObjectProperty.EssentiallySmall.{w, v, u} P →
    ∀ (hP : P.IsCardinalFilteredGenerator κ),
      ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
Tactic: obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
have obtain : ∀ (Q : ObjectProperty.{v, u} C),
  ObjectProperty.Small.{w, v, u} Q →
    ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure),
      ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
Tactic: obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le P
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)
have obtain : ∀ (P : ObjectProperty.{v, u} C),
  ObjectProperty.EssentiallySmall.{w, v, u} P →
    ∀ (hP : P.IsCardinalFilteredGenerator κ), ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)
Tactic: obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.ColimitPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : (j : J) → Category.{u_3, u_2} (I j)
D : Functor.{v_1, v, u_1, u} J C
P : (j : J) → ColimitPresentation.{u_3, u_2, v, u} (I j) (D.obj j)
k l m : Total (I := I) P
f : k.Hom (I := I) l
g : l.Hom (I := I) m
⊢ NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
      D.map (f.base (I := I) ≫ g.base (I := I)) =
    (f.hom (I := I) ≫ g.hom (I := I)) ≫
      NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
have simp : NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
    D.map (f.base (I := I)) ≫ D.map (g.base (I := I)) =
  f.hom (I := I) ≫
    g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
Tactic: simp only [Functor.const_obj_obj, Functor.map_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.ColimitPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : (j : J) → Category.{u_3, u_2} (I j)
D : Functor.{v_1, v, u_1, u} J C
P : (j : J) → ColimitPresentation.{u_3, u_2, v, u} (I j) (D.obj j)
k l m : Total (I := I) P
f : k.Hom (I := I) l
g : l.Hom (I := I) m
⊢ NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
      D.map (f.base (I := I)) ≫ D.map (g.base (I := I)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
have rw : f.hom (I := I) ≫
    NatTrans.app (ι (P (l.fst (β := fun (j : J) ↦ I j)))) (l.snd (β := fun (j : J) ↦ I j)) ≫ D.map (g.base (I := I)) =
  f.hom (I := I) ≫
    g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
Tactic: rw [f.w_assoc, g.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.ColimitPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : (j : J) → Category.{u_3, u_2} (I j)
D : Functor.{v_1, v, u_1, u} J C
P : (j : J) → ColimitPresentation.{u_3, u_2, v, u} (I j) (D.obj j)
k l m : Total (I := I) P
f : k.Hom (I := I) l
g : l.Hom (I := I) m
rw :
  f.hom (I := I) ≫
      NatTrans.app (ι (P (l.fst (β := fun (j : J) ↦ I j)))) (l.snd (β := fun (j : J) ↦ I j)) ≫ D.map (g.base (I := I)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
⊢ NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
      D.map (f.base (I := I)) ≫ D.map (g.base (I := I)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
have rw₁ : f.hom (I := I) ≫
    g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j)) =
  f.hom (I := I) ≫
    g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
Tactic: rw [f.w_assoc, g.w]