Interval simp normal forms

Stream: general

[Patrick Massot]

Should we have lemmas like:

@[simp] lemma Ici_def (x) : {t | x \le t} = Ici x := rfl

The point is the simp attribute. My goal is to have simp getting of as many interval manipulation as possible, including topological operation (like closure, interior and frontiers) of intervals.

[Patrick Massot]

And sometimes things are blocked because and interval is not written using I..

[Anatole Dedecker]

I totally second this. I'm still new to mathlib, but intervals are really frustrating : most useful lemmas are already there, but having to invoke them manually is quite annoying

[Johan Commelin]

Maybe one of the trickier but also most important enhancements would be the "simp procs" for simp?

[Johan Commelin]

It seems that this is necessary to bridge the step from a ≤ b to a < b in the hypothesis. (Currently simp won't trigger if you don't get the hyps exactly right...)