-- 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 : 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 : (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))
Tactic: choose k a hk using fun x ↦
          (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (congr_hom h x)