perf(analysis/complex/circle): fix a slow `@[simps]` (#17504)
This `@[simps]` is really slow on master and caused me a timeout in #17164, and moreover it generated a bad `simp` lemma (it used `↥(metric.sphere 0 1)` instead of `↥circle`), so I just wrote the lemma by hand.
