rel_embedding.coe_coe_fn

Stream: mathlib4

[Jeremy Tan]

On a side note, what's the mathlib4 equivalent of mathlib3 rel_embedding.coe_coe_fn? I apparently need it for a forwardport but coe_coe_fn does not appear in mathlib4 at all

[Jeremy Tan]

@[simp] lemma coe_coe_fn (f : r ↪r s) : ((f : r →r s) : α → β) = f := rfl

[Eric Wieser]

!4#3082

[Eric Wieser]

Please post things like this in a new topic next time, not in an unrelated topic. Just because a topic is busy doesn't mean you should post something unrelated in it.

[Jeremy Tan]

I don't see how !4#3082 can provide coe_coe_fn as a simp lemma

[Eric Wieser]

It's probably called coe_to_rel_hom there