-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Retracts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v, u} X κ
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
this_1 : EssentiallySmall.{w, w, w} J
this : IsFiltered J
refine_1 :
  ∀
    (f :
      Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
        (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)),
    ∃ (i : J) (xi : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj i)),
      f =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) i) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj i)) →
              (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj i))
          xi
⊢ IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op Y)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)
have refine_2 : ∀ (j : J) (f₁ f₂ : (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj j))
  (hf :
    Eq (α :=
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
          j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) j) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj j))
          f₁ :
        (fun (X : Type v) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
                (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)) j) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op Y)).mapCocone c).pt).obj j))
          f₂ :
        (fun (X : Type v) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op Y))
                (Functor.mapCocone (Functor.obj coyoneda (Opposite.op Y)) c)))
            j))),
  ∃ (k : J) (f : j ⟶ k),
    Eq (α := (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj k))
          f₁ :
        (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj k))
          f₂ :
        (fun (X : Type v) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op Y)).obj k))
Tactic: refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f₁ f₂ hf ↦ ?_)