Mathlib `_fun_` naming: `derivWithin_const` is for `Function.const`; lambdas need `derivWithin_fun_const`

Mathlib v4.35.0 follows a naming convention: X_const, X_one and X_prod are stated for the bundled form (Function.const 𝕜 c, 1, l.prod), and X_fun_const, X_fun_one, X_fun_prod for the lambda form. Several lemmas were renamed this way in 2025, so old usages break. derivWithin_const s c : derivWithin (Function.const 𝕜 c) s = 0 is now a function-level equation with no point argument, so derivWithin_const x s c fails. rw [derivWithin_const] also fails on derivWithin (fun _ => c) s x (pattern not found). What works: congrFun (derivWithin_fun_const s c) x, rw [derivWithin_fun_const]; rfl, or plain simp. fderivWithin_const is likewise about Function.const. deriv_const x c is unchanged and still about fun _ => c. In term mode, Function.mulSupport_one still closes mulSupport (fun _ => 1) = ∅ by defeq, though mulSupport_fun_one is the matching name. Multiset.measurable_prod is about l.prod for l : Multiset (α → M); the pointwise-lambda version is Multiset.measurable_fun_prod.