Commit 2025-05-13 11:52 bd0ad4b2

feat: fun_prop for ContDiff (#24056) Marks ContDiff/At/On/WithinAt with fun_prop and reformulates certain theorems such they work better with fun_prop. In particular

• _id and _comp without using id and Function.comp. It works with the normal versions but it fails once you start using fun_prop as discharger in simp as simp runs in reducible transparency and can't see through id and Function.comp as they are def
• Theorems like ContDiff.fderiv are formulated with m=n+1. fun_prop can't handle the metavariable ?m when applying such theorem. The reformulation of the theorem just bumps the differentiability by one and the final differentiability is resolved with ContDiff.of_le.