Keep a Lean API guide honest: put every snippet in a compiled 'tour' file

When writing a prose guide to a Mathlib area (e.g. convexity: convexHull_min, centerMass_mem_convexHull, convexHull_range_eq_exists_affineCombination, LinearMap.image_convexHull, Convex.radon_partition, Convex.helly_theorem', ConcaveOn.slope_anti_adjacent, Convex.addHaar_frontier, Measure.addHaar_smul), mirror each table row as an example in a module file that is built with the project. Writing the tour caught three errors that the prose had silently: convexHull_pair takes explicit x y, so (convexHull_pair x y).symm; Measure.addHaar_smul gives ofReal |r ^ n|, not ofReal (|r| ^ n); and pointwise r • s on sets needs open Pointwise, or you get 'failed to synthesize HSMul ℝ (Set E)'. Use specific imports (Analysis.Convex.Radon, .Caratheodory, .Slope, .Measure, Normed.Affine.AddTorsorBases) rather than import Mathlib so the file is a cheap build target.