`measurability` tactic cannot solve `MeasurableSet {x : ℝ | x > τ}`

[kalashnov]

Hi! My (almost) first experience with Mathlib. I want to report a very strange behavior of measurability tactic. Maybe there is some misunderstanding on my side, but I am moderately sure that this is a buggy behaviour.

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 advise on how to fix that, either deprioritize simp, or have more theorems for functions. What do you think?

import Mathlib
open MeasureTheory
open Set

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

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

-- 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