Confusing "MeasurableSet" display

Stream: new members

[Iocta]

import Mathlib

namespace MeasureTheory

open MeasurableSpace

variable {α : Type}

theorem generateFrom_mono' {s s' : Set (Set α)} (h : s ≤ s') :
    generateFrom s ≤ generateFrom s' := by
  intro t ht

displays as

ht : MeasurableSet t
⊢ MeasurableSet t

which is confusing. If I use

  reduce at ht
  reduce

then I can see

ht : GenerateMeasurable s t
⊢ GenerateMeasurable s' t

which is easier to understand. Is there a way to make this clearer display happen without me doing reduce every time?

[Kevin Buzzard]

If you hover over the terms you can see what's going on without unfolding

[Iocta]

I can't make it display like that normally?

[Kevin Buzzard]

set_option pp.implicit true or something like that should switch implicits on globally.

[Iocta]

set_option pp.explicit true is a little noisy but yeah that works

[Kevin Buzzard]

In general one would only expect one measurable space structure on a type so this isn't an issue. If you have more than one then I think it's just generally expected that you know what you're doing eg know the hover trick. Poor display will probably be the least of your worries -- typeclass synthesis being annoying will be more problematic