refactor: redefine `bundle.total_space` (#19221)
- Use a custom structure for `bundle.total_space`.
- Use `bundle.total_space.mk` instead of `bundle.total_space_mk`.
- Use `bundle.total_space.to_prod` instead of `equiv.sigma_equiv_prod`.
- Use `bundle.total_space.mk'` (scoped notation) to specify `F`.
- Rename `bundle.trivial.proj_snd` to
`bundle.total_space.trivial_snd` to allow dot notation. Should we
just use `bundle.total_space.snd` since `bundle.trivial` is now
reducible?
- Add an unused argument to `bundle.total_space`.
- Make `bundle.trivial` and `bundle.continuous_linear_map` reducible.
- Drop instances that are no longer needed.
