mathlib3

aabcd895 - chore(analysis/analytic_composition): weaken some typeclass arguments (#13924)

chore(analysis/analytic_composition): weaken some typeclass arguments (#13924) There's no need to do a long computation to show the multilinear_map is bounded, when continuity follows directly from the definition. This deletes `comp_along_composition_aux`, and moves the lemmas about the norm of `comp_along_composition` further down the file so as to get the lemmas with weaker typeclass requirements out of the way first. The norm proofs are essentially unchanged.