measurability regression

Stream: mathlib4

[Gareth Ma]

Mathlib 3:

import measure_theory.function.floor

example : measurable (λ (y : ℝ), int.fract y * y ⁻¹) :=
begin
  measurability
end

Mathlib 4:

import Mathlib.MeasureTheory.Function.Floor

example : Measurable (fun (y : ℝ) ↦ Int.fract y * y ⁻¹) := by
  measurability

fails with error

▶ 4:3-4:16: error:
tactic 'aesop' failed, failed to prove the goal after exhaustive search.
⊢ Measurable fun y => Int.fract y * y⁻¹

[Gareth Ma]

Am I missing some imports or something?

[Gareth Ma]

Solution is Measurable.mul measurable_fract measurable_inv

[Junyan Xu]

Possibly related: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Regression.20in.20continuity