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

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.