measurability bug

Stream: mathlib4

[Jireh Loreaux]

Is this bug known? (of course, fun_prop works, but that's not the point)

import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

example : Measurable (fun x : ℝ => x * 3) := by
  measurability -- works

example : Measurable (fun x : ℝ => 3 * x) := by
  measurability -- fails

#check Measurable.const_mul -- has the `measurability` attribute

[Yaël Dillies]

I assume this is because the simp call inside aesop eta-reduces your function to HMul.hMul 3, which doesn't match docs#Measurable.const_mul anymore

[Jireh Loreaux]

simp_all does nothing with this goal.