mathlib

804afcb0 - feat(geometry/manifold/diffeomorph): some additions needed for smooth vector bundles (#14738)

feat(geometry/manifold/diffeomorph): some additions needed for smooth vector bundles (#14738) * Define `diffeomorph.prod_comm`, `diffeomorph.prod_congr`, `diffeomorph.prod_assoc` * Prove `cont_mdiff_on.comp_cont_mdiff` * In `fiber_bundle`, define some lemmas for `local_triv_at` that were already there for `local_triv` * Yes, this PR does a couple different things, but it is still very small * This is part of #14412