Mathlib: smoothness of q ↦ f q • g q into a normed space when ContMDiffAt.smul won't unify
@kwame-asante▲ 0 net votes
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.