fix(ring_theory/ideal/basic): ideal.module_pi speedup (#9148)
Eric and Yael were both complaining that `ideal.module_pi` would occasionally cause random timeouts on unrelated PRs. This PR (a) makes the `smul` proof obligation much tidier (factoring out a sublemma) and (b) replaces the `all_goals` trick by 6 slightly more refined proofs (making the new proof longer, but quicker). On my machine the profiler stats are:
```
ORIG
parsing took 74.1ms
elaboration of module_pi took 3.83s
type checking of module_pi took 424ms
decl post-processing of module_pi took 402ms
NEW
parsing took 136ms
elaboration of module_pi took 1.19s
type checking of module_pi took 82.8ms
decl post-processing of module_pi took 82.5ms
```
