awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj j)
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
        j))
    ((hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj j))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
          j))
    ((hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj j))
        g :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
          j))
k : (x : ToType (FC := TypeCat.Fun) (unop (op X))) → J
a : (x_1 : ToType (FC := TypeCat.Fun) (unop (op X))) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) (unop (op X))),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          (f.hom'.toFun x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          (g.hom'.toFun x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
⊢ ∃ (k : J) (f_1 : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
      ((hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (op X)).map f_1) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj k))
          f :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
      ((hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (op X)).map f_1) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj k))
          g :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
have refine_2 : ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1
Tactic: dsimp at f g h k a hk ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := F.obj (k x_1))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) : (a : F.obj j) → F.obj (k x_1)) ((f.hom' : (a : X) → F.obj j) x_1) :
        F.obj (k x_1))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) : (a : F.obj j) → F.obj (k x_1)) ((g.hom' : (a : X) → F.obj j) x_1) :
        F.obj (k x_1))
⊢ ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1
have hk₁ : ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
    ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
        ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
      (fun (X : Type u) ↦ X) (F.obj (k x_1)))
    ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
        ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
      (fun (X : Type u) ↦ X) (F.obj (k x_1)))
Tactic: replace hk : ∀ x, F.map (a x) (f x) = F.map (a x) (g x) := by assumption
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
⊢ ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1
have refine_2 : ∀ (l : J) (b : j ⟶ l) (c : (x_1 : ToType (FC := TypeCat.Fun) X) → k x_1 ⟶ l)
  (hl : ∀ (x_1 : ToType (FC := TypeCat.Fun) X), a x_1 ≫ c x_1 = b),
  ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1
Tactic: obtain ⟨l, b, c, hl⟩ : ∃ (l : J) (c : j ⟶ l) (b : ∀ x, k x ⟶ l),
            ∀ x, a x ≫ b x = c := by
          let φ (x : X) : j ⟶ IsCardinalFiltered.max k hX :=
            a x ≫ IsCardinalFiltered.toMax k hX x
          exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c_1 : Cocone F
hc : IsColimit c_1
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c_1.ι.app j = g ≫ c_1.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
l : J
b : j ⟶ l
c : (x_1 : ToType (FC := TypeCat.Fun) X) → k x_1 ⟶ l
hl : ∀ (x_1 : ToType (FC := TypeCat.Fun) X), a x_1 ≫ c x_1 = b
⊢ f ≫ F.map b = g ≫ F.map b
have h₁ : ∀ (x_1 : X), (hom (FC := TypeCat.Fun) (f ≫ F.map b)).toFun x_1 = (hom (FC := TypeCat.Fun) (g ≫ F.map b)).toFun x_1
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
⊢ IsFilteredOrEmpty.{u, u} (HasCardinalLT.Set X κ)
have this : IsDirectedOrder.{u} (HasCardinalLT.Set X κ)
Tactic: have : IsDirectedOrder (HasCardinalLT.Set X κ) :=
      ⟨fun A B ↦ ⟨⟨A.val ∪ B.val, hasCardinalLT_union hκ A.prop B.prop⟩,
        Set.subset_union_left, Set.subset_union_right⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
⊢ Monotone.{u, u} (α := HasCardinalLT.Set X κ) (Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ))
have tauto : ∀ ⦃a b : HasCardinalLT.Set X κ⦄, a ≤ b → (↑a : Set X) ≤ (↑b : Set X)
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ ⦃a b : HasCardinalLT.Set X κ⦄, a ≤ b → (↑a : Set X) ≤ (↑b : Set X)
⊢ Monotone.{u, u} (α := HasCardinalLT.Set X κ) (Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ))
have tauto₅ : ∀ ⦃a b : HasCardinalLT.Set X κ⦄, a ≤ b → ∀ ⦃a_2 : X⦄, a_2 ∈ (↑a : Set X) → a_2 ∈ (↑b : Set X)
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
⊢ IsColimit (cocone X κ)
have this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
Tactic: have := isFiltered_of_aleph0_le X κ hκ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
⊢ IsColimit (cocone X κ)
have refine_1 : ∀ (x : (cocone X κ).pt),
  ∃ (i : HasCardinalLT.Set X κ) (xi : (fun (X : Type u) ↦ X) ((functor X κ).obj i)),
    x =
      (hom (FC := TypeCat.Fun) ((cocone X κ).ι.app i) :
          (a : (fun (X : Type u) ↦ X) ((functor X κ).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj i))
        xi
Tactic: refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
refine_1 :
  ∀ (x : (cocone X κ).pt),
    ∃ (i : HasCardinalLT.Set X κ) (xi : (fun (X : Type u) ↦ X) ((functor X κ).obj i)),
      x =
        (hom (FC := TypeCat.Fun) ((cocone X κ).ι.app i) :
            (a : (fun (X : Type u) ↦ X) ((functor X κ).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj i))
          xi
⊢ IsColimit (cocone X κ)
have refine_2 : ∀ (i : HasCardinalLT.Set X κ) (x y : (fun (X : Type u) ↦ X) ((functor X κ).obj i)),
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const (HasCardinalLT.Set X κ)) (cocone X κ).pt) i))
      ((hom (FC := TypeCat.Fun) ((cocone X κ).ι.app i) :
            (a : (fun (X : Type u) ↦ X) ((functor X κ).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj i))
          x :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const (HasCardinalLT.Set X κ)) (cocone X κ).pt) i))
      ((hom (FC := TypeCat.Fun) ((cocone X κ).ι.app i) :
            (a : (fun (X : Type u) ↦ X) ((functor X κ).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj i))
          y :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const (HasCardinalLT.Set X κ)) (cocone X κ).pt) i)) →
    ∃ (k : HasCardinalLT.Set X κ) (f : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) ((functor X κ).obj k))
        ((hom (FC := TypeCat.Fun) ((functor X κ).map f) :
              (a : (fun (X : Type u) ↦ X) ((functor X κ).obj i)) → (fun (X : Type u) ↦ X) ((functor X κ).obj k))
            x :
          (fun (X : Type u) ↦ X) ((functor X κ).obj k))
        ((hom (FC := TypeCat.Fun) ((functor X κ).map f) :
              (a : (fun (X : Type u) ↦ X) ((functor X κ).obj i)) → (fun (X : Type u) ↦ X) ((functor X κ).obj k))
            y :
          (fun (X : Type u) ↦ X) ((functor X κ).obj k))
Tactic: refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ ↔ HasCardinalLT X κ
have refine : IsCardinalPresentable X κ → HasCardinalLT X κ
Tactic: refine ⟨fun _ ↦ ?_, fun hX ↦ hX.isCardinalPresentable⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
⊢ HasCardinalLT X κ
have this : ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
  PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
Tactic: have := preservesColimitsOfShape_of_isCardinalPresentable X κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
⊢ HasCardinalLT X κ
have obtain : ∀ (A : Set X) (hA : HasCardinalLT (↑A : Type u) κ)
  (f :
    (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
      (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA))
  (hf :
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
      ((hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
                (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)) :
            (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (HasCardinalLT.Set X κ)).obj
                      ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                  ⟨A, hA⟩))
          f :
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := HasCardinalLT.Set X κ)
            (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
              (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
                (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
            (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
      (𝟙 X : X ⟶ X)),
  HasCardinalLT X κ
Tactic: obtain ⟨⟨A, hA⟩, f, hf⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (coyoneda.obj (op X))
      (HasCardinalLT.Set.isColimitCocone X κ
        (Cardinal.IsRegular.aleph0_le Fact.out))) (𝟙 X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
A : Set X
hA : HasCardinalLT (↑A : Type u) κ
f :
  (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
    (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := HasCardinalLT.Set X κ)
        (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
          (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
            (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
              (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)) :
          (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (HasCardinalLT.Set X κ)).obj
                    ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                ⟨A, hA⟩))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    (𝟙 X : X ⟶ X)
⊢ A = Set.univ
have h : ∀ (x : X), x ∈ A ↔ Membership.mem (γ := Set X) Set.univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
A : Set X
hA : HasCardinalLT (↑A : Type u) κ
f :
  (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
    (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := HasCardinalLT.Set X κ)
        (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
          (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
            (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
              (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)) :
          (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (HasCardinalLT.Set X κ)).obj
                    ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                ⟨A, hA⟩))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    (𝟙 X : X ⟶ X)
x : X
⊢ x ∈ A ↔ Membership.mem (γ := Set X) Set.univ x
have this₁ : Eq (α := (HasCardinalLT.Set.cocone X κ).pt)
  ((@hom _ types TypeCat.Fun _ _ _ _ _
          ((hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
                  (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)) :
              (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩)) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const (HasCardinalLT.Set X κ)).obj
                        ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                    ⟨A, hA⟩))
            f) :
        (a : unop (op X)) → (HasCardinalLT.Set.cocone X κ).pt)
      x :
    (HasCardinalLT.Set.cocone X κ).pt)
  ((hom (FC := TypeCat.Fun) (𝟙 X) : (a : unop (op X)) → (HasCardinalLT.Set.cocone X κ).pt) x :
    (HasCardinalLT.Set.cocone X κ).pt)
Tactic: have := congr_hom hf x
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this_1 :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
A : Set X
hA : HasCardinalLT (↑A : Type u) κ
f :
  (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
    (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := HasCardinalLT.Set X κ)
        (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
          (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
            (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
              (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)) :
          (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (HasCardinalLT.Set X κ)).obj
                    ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                ⟨A, hA⟩))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    (𝟙 X : X ⟶ X)
x : X
this : (↑((hom (FC := TypeCat.Fun) f : (a : X) → (↑A : Type u)) x) : X) = x
⊢ x ∈ A ↔ Membership.mem (γ := Set X) Set.univ x
have h : (↑((hom (FC := TypeCat.Fun) f : (a : X) → (↑A : Type u)) x) : X) ∈ A ↔
  Membership.mem (γ := Set X) Set.univ (↑((hom (FC := TypeCat.Fun) f : (a : X) → (↑A : Type u)) x) : X)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (goal)
Goal:
X_1 X : Type u
⊢ IsPresentable.{u, u, u + 1} X
have obtain : ∀ (κ : Cardinal.{u}) (hκ : κ.IsRegular) (hX : HasCardinalLT X κ), IsPresentable.{u, u, u + 1} X
Tactic: obtain ⟨κ, hκ, hX⟩ := HasCardinalLT.exists_regular_cardinal.{u} X
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X_1 X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
⊢ IsPresentable.{u, u, u + 1} X
have this : Fact κ.IsRegular
Tactic: have : Fact κ.IsRegular := ⟨hκ⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Type (hypothesis)
Goal:
X_1 X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this : Fact κ.IsRegular
⊢ IsPresentable.{u, u, u + 1} X
have this₁ : IsCardinalPresentable X κ
Tactic: have := hX.isCardinalPresentable
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f ↔ IsIso f.1 ∧ IsIso f.2
have mp : IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f → IsIso f.1 ∧ IsIso f.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Products.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
mp : IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f → IsIso f.1 ∧ IsIso f.2
⊢ IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f ↔ IsIso f.1 ∧ IsIso f.2
have mpr : IsIso f.1 ∧ IsIso f.2 → IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f
Tactic: constructor