Commit 2025-12-05 16:31 1ab85c21
View on Github →chore(Tactic/Measurability): fun_prop lemmas for solving MeasurableSet {x | ...} goals (#31592)
Currently, lemmas of the form MeasurableSet {x | ...} cannot be used by measurability, because simp changes the goal to Measurable fun x => .... This PR adds the necessary fun_prop lemmas so that they work with measurability (except for statements involving equality, which are done in #31512). This fixes #26620.