{S : Profinite} →
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} →
    CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op) →
      ((Condensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S))