[Merged by Bors] - refactor: redefine `bundle.total_space`

[urkud]

• 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.

---

• [x] depends on: #19223

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib#19223 By Dependent Issues (🤖). Happy coding!

[sgouezel]

Can you explain with more details why you needed to add the model fiber as an unused parameter to total_space? I.e., what goes wrong if you don't put it there?

[fpvandoorn]

I would also like to see some extra explanation about that. Besides that, this looks good to me.

[urkud]

I would also like to see some extra explanation about that. Besides that, this looks good to me.

Do you mean "see before merging to convince you that we should do this" or "added to the docstrings"? In the former case, see Zulip.

[fpvandoorn]

The former (though the latter would also be helpful). Thanks for the link. Let's go with this.

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests