-- 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)
⊢ HasCardinalLT X κ
have 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 κ
Tactic: obtain rfl : A = .univ := by
    ext x
    have := congr_hom hf x
    dsimp at this
    rw [← this]
    simp
Cleared hypotheses: A, hA, f, hf