orderDual defeq abuse

Stream: mathlib4

[Kim Morrison]

We still have quite a number of places in Mathlib where we are abusing the defeq of OrderDual.

One that I ran into today was docs#Dense.borel_eq_generateFrom_Ioc_mem_aux. Would anyone be interested in taking a look?

[Kim Morrison]

The first convert can be improved to

  convert hd.orderDual.borel_eq_generateFrom_Ico_mem_aux (by simpa using hbot)
    fun x y hlt he => hIoo (ofDual y) (ofDual x) hlt _ using 2

but this is still not right.

One can put seal OrderDual in above the declaration to ensure that defeq abuse is avoided! :-)