awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : 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 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x
hk :
  ∀ (x : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x)))
      ((hom (FC := TypeCat.Fun) (F.map (a x)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x) :
        (fun (X : Type u) ↦ X) (F.obj (k x)))
      ((hom (FC := TypeCat.Fun) (F.map (a x)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x) :
        (fun (X : Type u) ↦ X) (F.obj (k x)))
l : J
b : j ⟶ l
c : (x : ToType (FC := TypeCat.Fun) X) → k x ⟶ l
hl : ∀ (x : ToType (FC := TypeCat.Fun) X), a x ≫ c x = b
x : X
⊢ (hom (FC := TypeCat.Fun) (f ≫ F.map b)).toFun x = (hom (FC := TypeCat.Fun) (g ≫ F.map b)).toFun x

Tactic:
simp [← hl x, hk]
-- Module: Mathlib.CategoryTheory.Presentable.Type
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
⊢ ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1

Tactic:
refine ⟨l, b, by ext x; simp [← hl x, hk]⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
ι : Type u
A : ι → HasCardinalLT.Set X κ
hι rwa rwa₁ rwa₂ rwa₃ : Cardinal.mk ι < κ
⊢ HasCardinalLT ι κ

Tactic:
rwa [hasCardinalLT_iff_cardinal_mk_lt]

Premises used: hasCardinalLT_iff_cardinal_mk_lt
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
⊢ IsFiltered.{u, u} (HasCardinalLT.Set X κ)

Tactic:
isFiltered_of_isCardinalFiltered _ κ

Premises used: CategoryTheory.isFiltered_of_isCardinalFiltered
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
⊢ 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⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsDirectedOrder.{u} (HasCardinalLT.Set X κ)
⊢ IsFilteredOrEmpty.{u, u} (HasCardinalLT.Set X κ)

Tactic:
isFilteredOrEmpty_of_directed_le _

Premises used: CategoryTheory.isFilteredOrEmpty_of_directed_le
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsDirectedOrder.{u} (HasCardinalLT.Set X κ)
⊢ IsFilteredOrEmpty.{u, u} (HasCardinalLT.Set X κ)

Tactic:
exact isFilteredOrEmpty_of_directed_le _

Premises used: CategoryTheory.isFilteredOrEmpty_of_directed_le
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
tauto tauto₁ tauto₂ tauto₃ tauto₄ : ∀ ⦃a b : HasCardinalLT.Set X κ⦄, a ≤ b → (↑a : Set X) ≤ (↑b : Set X)
tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ tauto₁₁ tauto₁₂ tauto₁₃ :
  ∀ ⦃a b : HasCardinalLT.Set X κ⦄, a ≤ b → ∀ ⦃a_2 : X⦄, a_2 ∈ (↑a : Set X) → a_2 ∈ (↑b : Set X)
⊢ Monotone.{u, u} (α := HasCardinalLT.Set X κ) (Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ))

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
⊢ IsFiltered.{u, u} (HasCardinalLT.Set X κ)

Tactic:
have := isFiltered_of_aleph0_le X κ hκ
-- Module: Mathlib.CategoryTheory.Presentable.Type
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
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))
⊢ IsColimit (cocone X κ)

Tactic:
refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) ?_

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
x : (cocone X κ).pt
⊢ x ∈
    ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj
      (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) {x} ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
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:
exact ⟨⟨{x}, hasCardinalLT_of_finite _ _ hκ⟩, ⟨x, by simp⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
A : HasCardinalLT.Set X κ
x : X
hx : x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A
hy :
  Membership.mem (α := X) (⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A)
    ((hom (FC := TypeCat.Fun) ((cocone X κ).ι.app A) :
          (a : (fun (X : Type u) ↦ X) ((functor X κ).obj A)) →
            (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj A))
        (Subtype.mk (p := fun (x : X) ↦
          x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A) x hx) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const (HasCardinalLT.Set X κ)) (cocone X κ).pt) A))
⊢ ∃ (k : HasCardinalLT.Set X κ) (f : A ⟶ 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 A)) → (fun (X : Type u) ↦ X) ((functor X κ).obj k))
          (Subtype.mk (p := fun (x : X) ↦
            x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A) x hx) :
        (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 A)) → (fun (X : Type u) ↦ X) ((functor X κ).obj k))
          (Subtype.mk (p := fun (x : X) ↦
            x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A)
            ((hom (FC := TypeCat.Fun) ((cocone X κ).ι.app A) :
                (a : (fun (X : Type u) ↦ X) ((functor X κ).obj A)) →
                  (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj A))
              (Subtype.mk (p := fun (x : X) ↦
                x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A) x hx))
            hy) :
        (fun (X : Type u) ↦ X) ((functor X κ).obj k))

Tactic:
⟨A, 𝟙 _, rfl⟩

Premises used: CategoryTheory.CategoryStruct.id, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered.{u, u} (HasCardinalLT.Set X κ)
A : HasCardinalLT.Set X κ
x : X
hx : x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A
hy :
  Membership.mem (α := X) (⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A)
    ((hom (FC := TypeCat.Fun) ((cocone X κ).ι.app A) :
          (a : (fun (X : Type u) ↦ X) ((functor X κ).obj A)) →
            (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj A))
        (Subtype.mk (p := fun (x : X) ↦
          x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A) x hx) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const (HasCardinalLT.Set X κ)) (cocone X κ).pt) A))
⊢ ∃ (k : HasCardinalLT.Set X κ) (f : A ⟶ 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 A)) → (fun (X : Type u) ↦ X) ((functor X κ).obj k))
          (Subtype.mk (p := fun (x : X) ↦
            x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A) x hx) :
        (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 A)) → (fun (X : Type u) ↦ X) ((functor X κ).obj k))
          (Subtype.mk (p := fun (x : X) ↦
            x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A)
            ((hom (FC := TypeCat.Fun) ((cocone X κ).ι.app A) :
                (a : (fun (X : Type u) ↦ X) ((functor X κ).obj A)) →
                  (fun (X : Type u) ↦ X) (((Functor.const (HasCardinalLT.Set X κ)).obj (cocone X κ).pt).obj A))
              (Subtype.mk (p := fun (x : X) ↦
                x ∈ ⋯.functor (f := Subtype.val (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ)).obj A) x hx))
            hy) :
        (fun (X : Type u) ↦ X) ((functor X κ).obj k))

Tactic:
exact ⟨A, 𝟙 _, rfl⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ ↔ HasCardinalLT X κ

Tactic:
⟨fun _ ↦ ?_, fun hX ↦ hX.isCardinalPresentable⟩

Premises used: Iff.intro, HasCardinalLT.isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
refine : IsCardinalPresentable X κ → HasCardinalLT X κ
⊢ IsCardinalPresentable X κ ↔ HasCardinalLT X κ

Tactic:
refine ⟨fun _ ↦ ?_, fun hX ↦ hX.isCardinalPresentable⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
⊢ ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable X κ
-- Module: Mathlib.CategoryTheory.Presentable.Type
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))
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 κ
⊢ 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)

Premises used: CategoryTheory.coyoneda, Cardinal.IsRegular.aleph0_le, CategoryTheory.CategoryStruct.id, HasCardinalLT.Set.isColimitCocone, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, Opposite.op, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h_1 : 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)
h : ∀ (x : X), x ∈ A ↔ Membership.mem (γ := Set X) Set.univ x
⊢ A = Set.univ

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Presentable.Type
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h_1 : 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
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)
⊢ x ∈ A ↔ Membership.mem (γ := Set X) Set.univ x

Tactic:
rw [← this]