feat(data/real/basic): remove typeclass shortcircuit (#17804)
The only remaining use of `module` in `data/real/basic` and its prerequisites is to provide the typeclass shortcircuit
```lean
instance : module ℝ ℝ := by apply_instance
```
I propose deleting this.
