OrderIso toFun

Stream: mathlib4

[Chris Hughes]

If I coerce an OrderIso to a function I get a nasty looking term displayed

import Mathlib.Order.Hom.Bounded

example {α β : Type _} [PartialOrder α] [PartialOrder β]
    (f : α ≃o β) (a : α) : f a = sorry := by
  -- ↑(RelIso.toRelEmbedding f).toEmbedding a = sorryAx ((fun x => β) a)

I guess there needs to be some tidy up somewhere, but I haven't figured it out exactly yet. It seems to be causing some rewrites to fail in !4#3036

[Arien Malec]

I think I put the trick to this in the wiki

[Arien Malec]

I did!

[Eric Wieser]

docs#rel_embedding.coe_fn_to_embedding should be applying (edit: if you dsimp)

[Eric Wieser]

docs4#RelIso.instCoeFunRelIsoForAll is to blame

[Eric Wieser]

That should be removed or implemented with FunLike.coe

[Chris Hughes]

Thanks for figuring that out