chore(*): rename default to basic (#17724)
This renames four "contentful" files from `default.lean` to `basic.lean`. I also verified (I think) that we import no `default.lean` files in mathlib, besides those under `tactic/`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
