Measurability cannot prove `MeasurableSet {x : ℝ | x > τ}

Stream: mathlib4

[Michael Rothgang]

I just saw #26620 --- let me cross-post this here for visibility:

[Michael Rothgang]

import Mathlib
open MeasureTheory
open Set

theorem greaterSet (τ : ℝ) :
  MeasurableSet {x : ℝ | x > τ} := by
  measurability

-- both fail with the same problem:
-- tactic 'aesop' failed, failed to prove the goal after exhaustive search.
-- Initial goal:

-- τ : ℝ
-- ⊢ MeasurableSet {x | x > τ}
-- Remaining goals after safe rules:

-- τ : ℝ
-- ⊢ Measurable (LT.lt τ)

-- My own proof of the statement
theorem greaterSet'' (τ : ℝ) :
  MeasurableSet {x : ℝ | x > τ} := by
  exact measurableSet_Ioi
-- Here I first prove that {x : ℝ | x > τ} is Ioi and then measurability passes through, avoiding casting to function
theorem greaterSet_with_measurability (τ : ℝ) :
  MeasurableSet {x : ℝ | x > τ} := by
  have : {x : ℝ | x > τ} = Ioi τ := by
    ext x
    simp [Ioi, mem_setOf_eq]
  rw [this]
  measurability
-- Now I redefine measurability and disable simp. The proof goes through.
macro "measurability" : tactic =>
  `(tactic| aesop (config := { terminal := true, enableSimp := false })
    (rule_sets := [$(Lean.mkIdent `Measurable):ident]))

theorem greaterSet''' (τ : ℝ) :
  MeasurableSet {x : ℝ | x > τ} := by
  measurability

[Michael Rothgang]

The problem is that measurability cannot prove a very simple, almost definitional MeasurableSet because it first applies simp and gets a Measurable function instead of a set, which it cannot prove

I have redefined the measurability to add enableSimp := false and it works.

Cannot give any advice on how to fix that, either deprioritize simp, or have more theorems for functions. What do you think?

[Michael Rothgang]

(To repeat, I did not create this issue --- but am also curious why this is.)

[Michael Rothgang]

Replacing ">" by "<" makes no difference here.

[David Ledvinka]

I did some investigation

import Mathlib
open MeasureTheory
open Set

theorem greaterSet (τ : ℝ) :
  MeasurableSet {x : ℝ | x > τ} := by
  measurability?
  /- simp_all only [gt_iff_lt, measurableSet_setOf]
     sorry -/

attribute [-simp] gt_iff_lt
attribute [-simp] measurableSet_setOf

theorem greaterSet' (τ : ℝ) :
    MeasurableSet {x : ℝ | x > τ} := by
  measurability?
  /- apply measurableSet_lt
     · simp_all only [measurable_const]
     · apply measurable_id'-/

theorem greaterSet'' (τ : ℝ) :
    MeasurableSet {x : ℝ | τ < x} := by
  measurability?
  /- sorry -/

theorem greaterSet''' (τ : ℝ) :
    MeasurableSet {x : ℝ | τ < x} := by
  apply measurableSet_lt
  · simp_all only [measurable_const]
  · apply measurable_id'

If you remove the simp lemmas that measurability uses then it works but notably it doesn't work when you flip the sign (and this is also true when you disable simp). I think probably MeasurableSet_SetOf shouldn't be a simp lemma (instead the direction that is used should be made into a measurability lemma) but this still doesn't fix the issue. Of course if we can get measurability to work for the lt sign case then we wouldnt need to remove gt_iff_lt from simp. Note its weird that measurability cant prove the lt case after removing the simp lemmas since the exact proof that measurability finds for the gt case works for the lt case. I don't (yet) have an understanding of how aesop works to diagnose why this happens but I have ran into a few weird cases like this and I am in the process of learning meta programming in part so I can try to improve measurability and fun_prop.

[Georgy Kalashnov]

Michael, thanks for endorsing this! And thanks for debugging that, David.

I have a more general question on the matter though. I do not really understand, why MeasurableSet is not a class (in the same way MeasurableSpace or IsMarkovKernel are) with some instances (which are now theorems marked with measurability tag), which can automatically infer (and therefore prove) MeasurableSet and Measurable statements.

This would be so useful for defs and theorems using random variables, I have some examples and arguments, but maybe the answer is simple and I won't overwhelm the thread