∀ {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))}
  (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)),
  Condensed.lanPresheafIso hF =
    (CategoryTheory.Functor.Final.colimitIso (Profinite.Extend.functorOp S.asLimitCone)
          ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp
            (FintypeCat.toProfinite.op.comp F))).symm ≪≫
      (CategoryTheory.Limits.colimit.isColimit (S.diagram.op.comp F)).coconePointUniqueUpToIso hF