mathlib3

88f8de36 - feat(topology/local_homeomorph): define helper definition (#14360)

feat(topology/local_homeomorph): define helper definition (#14360) * Define `homeomorph.trans_local_homeomorph` and `local_homeomorph.trans_homeomorph`. They are equal to `local_homeomorph.trans`, but with better definitional behavior for `source` and `target`. * Define similar operations for `local_equiv`. * Use this to improve the definitional behavior of [`topological_fiber_bundle.trivialization.trans_fiber_homeomorph`](https://leanprover-community.github.io/mathlib_docs/find/topological_fiber_bundle.trivialization.trans_fiber_homeomorph) * Also use `@[simps]` to generate a couple of extra simp-lemmas.