mathlib3

01876449 - feat(geometry/manifold/vector_bundle/tangent): use the new tangent bundle definition in the library (#18601)

feat(geometry/manifold/vector_bundle/tangent): use the new tangent bundle definition in the library (#18601) * Stop using the old tangent bundle definition, and use the new one instead * This affects `geometry.manifold.mfderiv` and later files. * We remove `cont_mdiff_at_iff_target`, which doesn't hold anymore in the new setting. * We prove `cont_mdiff_at_total_space`, which characterizes `C^n` maps into a vector bundle. We need a bunch of basic lemmas to prove this. This makes it easy to prove `smooth_zero_section`. * We move some results from `cont_mdiff_mfderiv` to `manifold/vector_bundle/basic`