Michael Stoll suggests it on https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Summable.20for.20functions.20on.20product/near/484051430