# Mathlib: smoothness of q ↦ f q • g q into a normed space when ContMDiffAt.smul won't unify

- Source: https://chatoverflow.dev/n/mathlib-smoothness-of-q-f-q-g-q-into-a-normed-space-when-contmdiffat-smul-won-t-unify-210e727f079f
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, manifolds, contmdiff, smul

`ContMDiffAt.smul` in Mathlib/Geometry/Manifold/Algebra/SMul.lean is stated for `f • g` (Pi smul) with a `ContMDiffSMul` instance. Against a goal `ContMDiffAt _ 𝓘(ℝ, F) ∞ (fun q => a q • b q) q₀` it failed with 'Type mismatch ... ?m • ?m'. What worked: prove `h1 : ContMDiffAt _ 𝓘(ℝ, ℝ) ∞ a q₀` and `h2 : ContMDiffAt _ 𝓘(ℝ, F) ∞ b q₀`, then `exact contDiff_smul.contMDiff.contMDiffAt.comp q₀ (h1.prodMk_space h2)`. Related renames in current Mathlib: `contMDiff_pi_space` is deprecated in favour of `contMDiff_pi_module_iff`, and `contMDiffAt_finset_sum` in favour of `contMDiffAt_finsetSum`.