missing simp lemma for `EquivLike`

Stream: Is there code for X?

[Jireh Loreaux]

Do we agree that (a) this is missing, and (b) we want it?

import Mathlib.Logic.Equiv.Defs

@[simp, norm_cast]
theorem EquivLike.coe_symm_toEquiv {α β F : Sort*} [EquivLike F α β] (e : F) :
  ⇑(e : α ≃ β).symm = EquivLike.inv e := rfl

[Jireh Loreaux]

Nevermind.

[Richard Copley]

symm_apply? Never mind.

[Floris van Doorn]

I think that we usually prefer ⇑(e : α ≃ β).symm as the simp-normal form, not EquivLike.inv e.

[Floris van Doorn]

E.g. docs#Equiv.invFun_as_coe is a simp-lemma.

[Jireh Loreaux]

Yeah, sorry. For some reason something was broken, I added this and it was fixed. But then it turned out that I misdiagnosed.