chore: match the definition of AnalyticWithinAt with `ContDiffWithi…

…nAt` (#16725)

The current definition of `AnalyticWithinAt` in a set `s` at a point `x` requires good behavior inside `s`, and continuity within `s` at `x` (because good behavior at `x` is important). In `ContDiffWithinAt`, where the issues are similar, one requires instead good behavior inside `insert x s`. Those two points of view are equivalent, but the latter is often more convenient (just one field to check, more uniform proofs). 

In this PR, we switch the definition of `AnalyticWithinAt` to the latter approach. We also expand a little bit the API around `AnalyticWithinAt`, by tweaking theorems that required `AnalyticAt` to require `AnalyticWithinAt`, and deduce `AnalyticAt` versions from `AnalyticWithinAt` versions. For this, a few statements have to be moved from the file `Analytic.Within.lean` to `Analytic.Basic.lean`.

There is no real new statement or new proof in this PR, but it opens the way to further improvements.