Commit 2025-12-04 16:59 fcb0760f

chore: replace some @[measurability] attributes by @[fun_prop] (#32187) Since #30511, the @[measurability] attribute applies @[fun_prop] when applied to statements about Measurable. This PR cleans up some of these attributes. There are two types of change in this PR, neither of which change the behavior of tactics:

• Changing @[measurability] to @[fun_prop]: this has no effect.
• Changing @[fun_prop, measurability] to @[fun_prop]: this just removes a duplicate fun_prop theorem. Note that this PR does not change the attributes of lemmas where it was unclear whether they should be tagged with fun_prop.