awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
J : Type w
inst_6 : SmallCategory J
inst_7 : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))
have this : PreservesColimitsOfShape.{w, w, v', v', u', v' + 1} J (Functor.obj coyoneda (op M))
Tactic: have := preservesColimitsOfShape_of_isCardinalPresentable M κ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
hP : P.IsStrongGenerator
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
⊢ ObjectProperty.IsStrongGenerator (C := Functor.{w, v', w, u'} Cᵒᵖ A)
    (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A))
have rw : ∀
  (hP :
    P.IsSeparating ∧
      ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
        (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i)
  [inst_4 : HasCoproducts.{w, v', u'} A] [HasPullbacks.{v', u'} A] (C : Type w) [inst_6 : SmallCategory C],
  ObjectProperty.IsSeparating (C := Functor.{w, v', w, u'} Cᵒᵖ A)
      (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) ∧
    ∀ ⦃X Y : Functor.{w, v', w, u'} Cᵒᵖ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
          ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
            Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) →
        IsIso i
Tactic: rw [ObjectProperty.isStrongGenerator_iff] at hP ⊢
Cleared hypotheses: hP, inst_1, inst_2, C, inst_3
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (hypothesis)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
hP :
  P.IsSeparating ∧
    ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
⊢ ObjectProperty.IsSeparating (C := Functor.{w, v', w, u'} Cᵒᵖ A)
      (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) ∧
    ∀ ⦃X Y : Functor.{w, v', w, u'} Cᵒᵖ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
          ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
            Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) →
        IsIso i
have hP₁ : P.IsSeparating
Tactic: obtain ⟨hP₁, hP₂⟩ := hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (hypothesis)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
hP :
  P.IsSeparating ∧
    ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
⊢ ObjectProperty.IsSeparating (C := Functor.{w, v', w, u'} Cᵒᵖ A)
      (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) ∧
    ∀ ⦃X Y : Functor.{w, v', w, u'} Cᵒᵖ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
          ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
            Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) →
        IsIso i
have hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
Tactic: obtain ⟨hP₁, hP₂⟩ := hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
⊢ ObjectProperty.IsSeparating (C := Functor.{w, v', w, u'} Cᵒᵖ A)
      (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) ∧
    ∀ ⦃X Y : Functor.{w, v', w, u'} Cᵒᵖ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
          ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
            Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) →
        IsIso i
have refine : ∀ (P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A) (i : P₁ ⟶ P₂),
  Mono i →
    ∀
      (hi :
        ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
          ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
            Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i),
      IsIso i
Tactic: refine ⟨Presheaf.isSeparating (C := C) (ι := Subtype P) (S := Subtype.val)
    (by simpa using hP₁),
    fun P₁ P₂ i _ hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
⊢ IsIso i
have rw : ∀ (X : Cᵒᵖ), IsIso (i.app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
⊢ IsIso (X := P₁.obj (op X)) (i.app (op X))
have refine : ∀ (G : A) (hG : P G) (f : G ⟶ P₂.obj (op X)),
  ∃ (a : G ⟶ P₁.obj (op X)), (fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a = f
Tactic: refine hP₂ _ (fun G hG f ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
G : A
hG : P G
f : G ⟶ P₂.obj (op X)
⊢ ∃ (a : G ⟶ P₁.obj (op X)), (fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a = f
have obtain : ∀ (y : freeYoneda X G ⟶ P₂),
  ∃ (a : G ⟶ P₁.obj (op X)),
    Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a : G ⟶ P₂.obj (op X))
      ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) y : G ⟶ P₂.obj (op X))
Tactic: obtain ⟨y, rfl⟩ := freeYonedaHomEquiv.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
G : A
hG : P G
y : freeYoneda X G ⟶ P₂
⊢ ∃ (a : G ⟶ P₁.obj (op X)),
    Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a : G ⟶ P₂.obj (op X))
      ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) y : G ⟶ P₂.obj (op X))
have obtain : ∀ (x : freeYoneda X G ⟶ P₁),
  ∃ (a : G ⟶ P₁.obj (op X)),
    Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a)
      ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) ((fun (f : freeYoneda X G ⟶ P₁) ↦ f ≫ i) x))
Tactic: obtain ⟨x, rfl⟩ := hi (freeYoneda X G)
    (ObjectProperty.ofObj_apply (fun (T : C × (Subtype P)) ↦
      freeYoneda T.1 T.2.1) ⟨X, G, hG⟩) y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (hypothesis)
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
⊢ IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
have hA : ∃ (P : ObjectProperty.{v', u'} A) (_ : ObjectProperty.Small.{w, v', u'} P),
  P.IsStrongGenerator ∧ P ≤ isCardinalPresentable A κ
Tactic: have hA := (IsCardinalLocallyPresentable.iff_exists_isStrongGenerator A κ).1 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
hA :
  ∃ (P : ObjectProperty.{v', u'} A) (_ : ObjectProperty.Small.{w, v', u'} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable A κ
⊢ IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
have obtain : ∀ (P : ObjectProperty.{v', u'} A),
  ObjectProperty.Small.{w, v', u'} P →
    ∀ (hP₁ : P.IsStrongGenerator) (hP₂ : P ≤ isCardinalPresentable A κ),
      IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
Tactic: obtain ⟨P, _, hP₁, hP₂⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
have rw : ∃ (P : ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A)) (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
  P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
Tactic: rw [IsCardinalLocallyPresentable.iff_exists_isStrongGenerator]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ ∃ (P : ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A)) (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
have refine : LE.le (α := ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A))
  (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A))
  (isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ)
Tactic: refine ⟨_, inferInstance, isStrongGenerator hP₁ C, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (hypothesis)
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
⊢ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
    (freeYoneda (X, Subtype.mk (p := P) G hG).1 (↑(X, Subtype.mk (p := P) G hG).2 : A))
have this : isCardinalPresentable.{w, v', u'} A κ G
Tactic: have := hP₂ _ hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (hypothesis)
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
this : isCardinalPresentable.{w, v', u'} A κ G
⊢ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
    (freeYoneda (X, Subtype.mk (p := P) G hG).1 (↑(X, Subtype.mk (p := P) G hG).2 : A))
have this₁ : IsCardinalPresentable.{w, v', u'} G κ
Tactic: rw [isCardinalPresentable_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
A : Type u'
inst : Category.{v', u'} A
inst_1 : IsLocallyPresentable.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
have obtain : ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular),
  IsCardinalLocallyPresentable.{w, v', u'} A κ →
    ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
Tactic: obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} A
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
have this : EssentiallySmall.{w, w, w} J
Tactic: have := essentiallySmallSelf J
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this : EssentiallySmall.{w, w, w} J
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
have this₁ : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
have refine_1 : ∀
  (f :
    Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
      (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)),
  ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
        xi
Tactic: refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f₁ f₂ hf ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
⊢ ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
        xi
have refine_1 : ∀ (i : J) (g : X ⟶ F.obj i) (hg : g ≫ c.ι.app i = h.r ≫ f),
  ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
        xi
Tactic: obtain ⟨i, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ hc (h.r ≫ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj j)
hf :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
            (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
        j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) j) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj j))
        f₁ :
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
          j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) j) :
          (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
            (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj j))
        f₂ :
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
          j))
⊢ ∃ (k : J) (f : j ⟶ k),
    Eq (α := (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj k))
          f₁ :
        (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj k))
          f₂ :
        (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
have refine_2 : ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f
Tactic: dsimp at f₁ f₂ hf ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : Y ⟶ F.obj j
hf : f₁ ≫ c.ι.app j = f₂ ≫ c.ι.app j
⊢ ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f
have refine_2 : ∀ (k : J) (u : j ⟶ k) (hj : (h.r ≫ f₁) ≫ F.map u = (h.r ≫ f₂) ≫ F.map u),
  ∃ (k : J) (f : j ⟶ k), f₁ ≫ F.map f = f₂ ≫ F.map f
Tactic: obtain ⟨k, u, hj⟩ := IsCardinalPresentable.exists_eq_of_isColimit'
        κ hc (h.r ≫ f₁) (h.r ≫ f₂) (by simp [hf])
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
Y X : C
h : Retract Y X
hX : isCardinalPresentable.{w, v, u} C κ X
⊢ isCardinalPresentable.{w, v, u} C κ Y
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
inst_1 : LocallySmall.{w, v, u} C
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
F : Functor.{v', v, u', u} J C
inst_4 : F.IsDense
κ : Cardinal.{w}
inst_5 : Fact κ.IsRegular
inst_6 : ∀ (j : J), IsCardinalPresentable.{w, v, u} (F.obj j) κ
inst_7 : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
⊢ ∃ (J_1 : Type w) (x : SmallCategory J_1) (_ : IsCardinalFiltered J_1 κ),
    (ObjectProperty.map ⊤ F).colimitsOfShape J_1 X
have have : ∀ (ip : F.DenseAt X),
  ∃ (J_1 : Type w) (x : SmallCategory J_1) (_ : IsCardinalFiltered J_1 κ),
    (ObjectProperty.map ⊤ F).colimitsOfShape J_1 X
Tactic: have ip := F.denseAt X