measurability shortcomings

[LorenzoLuccioli]

Instances where the tactic measurability should work, but it doesn't.

This is one example, if I find more I will add them to this issue:

example {ι : Type*} [Fintype ι] {β : ι → Type*} [∀ i, MeasurableSpace (β i)]
    (s : (i : ι) → Set (β i)) (h : ∀ i, MeasurableSet (s i)) :
    MeasurableSet (Set.pi Set.univ s) := by
  -- measurability
  exact MeasurableSet.univ_pi h

In this case measurability doesn't manage to prove that the product of the Set.univ is measurable. It doesn't work eve if we add the @[measurability] attribute to MeasurableSet.univ_pi.

[LorenzoLuccioli]

In this case it doesn't manage to prove that the set where a measurable function is different from zero is measurable.

example (g : ℝ → ℝ) (h : Measurable g) : MeasurableSet {x | g x ≠ 0} := by
  rw [show {x | g x ≠ 0} = g ⁻¹' {x | x ≠ 0} by simp]
  apply h
  simp only [ne_eq, Set.compl_ne_eq_singleton, MeasurableSet.compl_iff, MeasurableSet.singleton,
    MeasurableSet.compl_iff.mp]

[RemyDegenne]

This does not alter the fact that the measurability tactic is failing, but you might want to know that that second example has a very short proof:

example (g : ℝ → ℝ) (h : Measurable g) : MeasurableSet {x | g x ≠ 0} :=
  h (measurableSet_singleton _).compl