feat(Condensed): colimit characterization of discrete condensed sets (#15566)

This PR provides the necessary API to prove that a condensed set `X` is discrete if and only if
for every profinite set `S = limᵢSᵢ`, `X(S) ≅ colimᵢX(Sᵢ)`, and the analogous result for light
condensed sets.

Author: dagurtomas

Mathlib.lean

@@ -2075,6 +2075,7 @@ import Mathlib.Computability.TuringMachine
 import Mathlib.Condensed.Basic
 import Mathlib.Condensed.CartesianClosed
 import Mathlib.Condensed.Discrete.Basic
+import Mathlib.Condensed.Discrete.Colimit
 import Mathlib.Condensed.Discrete.LocallyConstant
 import Mathlib.Condensed.Discrete.Module
 import Mathlib.Condensed.Epi