Commit 2023-04-20 06:30 c8b10b06

chore: use FunLike.coe as coercion for OrderIso and RelEmbedding (#3082) The changes I made were. Use FunLike.coe instead of the previous definition for the coercion from RelEmbedding To functions and OrderIso to functions. The previous definition was

instance : CoeFun (r ↪r s) fun _ => α → β :=
--   ⟨fun o => o.toEmbedding⟩

This does not display nicely. I also restored the simp attributes on a few lemmas that had their simp attributes removed during the port. Eventually we might want a RelEmbeddingLike class, but this PR does not implement that. I also added a few lemmas that proved that coercions to function commute with RelEmbedding.toRelHom or similar. The other changes are just fixing the build. One strange issue is that the lemma Finset.mapEmbedding_apply seems to be harder to use, it has to be used with rw instead of simp