diff --git a/src/examples/profinite.lean b/src/examples/cond.lean
similarity index 95%
rename from src/examples/profinite.lean
rename to src/examples/cond.lean
index 5396060e..3f80b987 100644
--- a/src/examples/profinite.lean
+++ b/src/examples/cond.lean
@@ -1,5 +1,15 @@
 import challenge
 
+/-!
+
+The main goal of this file is to discuss the definition of
+condensed abelian groups which is used in this project.
+
+As prerequisites, we also discuss continuous maps and the
+category of profinite sets.
+
+-/
+
 open category_theory category_theory.limits opposite
 open_locale liquid_tensor_experiment