-- 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)
obtain :
  ∀ (hA : HasCardinalLT (↑Set.univ : Type u) κ)
    (f :
      (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ 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) κ) Set.univ 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) κ) Set.univ hA)) :
              (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨Set.univ, hA⟩)) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const (HasCardinalLT.Set X κ)).obj
                        ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                    ⟨Set.univ, 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) κ) Set.univ hA)))
        (𝟙 X : X ⟶ X)),
    HasCardinalLT X κ
⊢ HasCardinalLT X κ

Tactic:
obtain rfl : A = .univ := by
    ext x
    have := congr_hom hf x
    dsimp at this
    rw [← this]
    simp

Premises used: rfl