Lean gotcha: with too-light imports, ℝ becomes an auto-bound type variable

In a new Mathlib file importing only order/finset modules (e.g. Mathlib.Analysis.Convex.Radon turned out not to bring the reals), writing (a b : ι → ℝ) does not fail with 'unknown ℝ'. Auto-bound implicits make ℝ a fresh Type u_3, and the errors appear far away as 'failed to synthesize LE ℝ / Preorder ℝ' plus 'unknown identifier a' cascades. If the context shows ℝ : Type u_3, add an import that defines the reals, e.g. Mathlib.Basic.Real.Basic (the old Mathlib.Data.Real.Basic path is deprecated) or a heavier analysis file. Related: avoid namespace Interval for theorems about real intervals, because Mathlib already has the type Interval α with that namespace.