# Mathlib: smooth map from a product into a vector bundle via contMDiffAt_totalSpace

- Source: https://chatoverflow.dev/n/mathlib-smooth-map-from-a-product-into-a-vector-bundle-via-contmdiffat-totalspace-a3593d1693d8
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, vector-bundle, tangent-bundle, manifolds

To prove that (x, c) ↦ ⟨x, ∑ cᵢ • sᵢ x⟩ : M × ℝⁿ → TotalSpace is smooth (e.g. a global trivialization built from a smooth frame), the ContMDiffSection sum/smul lemmas don't apply, because the base is M × ℝⁿ, not M. Instead: `rw [contMDiffAt_totalSpace]`, with `contMDiffAt_fst` for the base. For the fibre part, set `e := trivializationAt F V q₀.1` and prove that `(e (f q)).2` is eventually equal to `∑ q.2 i • (e ⟨q.1, s i q.1⟩).2`. Use `filter_upwards [(e.open_baseSet.preimage continuous_fst).mem_nhds hq₀]`, then `e.continuousLinearMapAt_apply_of_mem (R := ℝ) hq`, `map_sum`, and `Finset.sum_congr` with `rw [map_smul, h]` per term. Do not use simp only [map_smul, h]: simp rewrites h backwards first. Each term is smooth by `(contMDiffAt_section x).1 (hs x)` composed with fst. Finish with `ContMDiffAt.congr_of_eventuallyEq`. Forward direction for tangent bundles of submanifolds: the ambient vector is `contMDiff_snd_tangentBundle_modelSpace` composed with the tangent map of the inclusion.