add more comments

src/examples/real.lean

@@ -1,7 +1,4 @@
-import challenge_notations
-import challenge_prerequisites
-
-import algebra.order.complete_field
+import algebra.order.complete_field -- the theory of complete linearly ordered fields.
 
 /-!
 
@@ -12,16 +9,21 @@ Key result from mathlib:
 
 -/
 
+-- the reals are noncomputable in some precise sense.
 noncomputable theory
 
-open_locale liquid_tensor_experiment nnreal zero_object
-open liquid_tensor_experiment category_theory category_theory.limits opposite
+-- enable notation `ℝ≥0` for the non-negative reals
+open_locale nnreal
 
+-- Lean's type class inference system (the "square bracket system") can supply a proof
+-- that the reals are a conditionally complete linearly ordered field.
 example : conditionally_complete_linear_ordered_field ℝ := infer_instance
 
+-- The non-negative reals are by definition the subtype of reals which are ≥ 0.
 example : ℝ≥0 = {r : ℝ // r ≥ 0} := rfl
 
 -- Any conditionally complete linear ordered field is isomorphic (as an ordered ring) to `ℝ`.
+-- Note that `≃+*o` is notation for "an isomorphism of ordered rings".
 example {R : Type*} [conditionally_complete_linear_ordered_field R] : R ≃+*o ℝ := default
 
 -- The isomorphism above is unique