Equiv.symm as Equiv.

Stream: Is there code for X?

[Wrenna Robson]

import Mathlib.Logic.Equiv.Defs

/-- `EquivLike.symm` defines an equivalence between `α ≃ β` and `β ≃ α`. -/
@[simps!]
def equivSymm : (α ≃ β) ≃ (β ≃ α) where
  toFun := Equiv.symm
  invFun := Equiv.symm

I can't believe we don't have this but I can't seem to find it.

[Miyahara Kō]

I couldn't find it with Loogle either.
Since Mathlib has developed by gradually adding definitions as they become necessary, it's not uncommon for some definitions or theorems — even ones that feel like "I can't believe this isn't here" — to be missing.
If you come across something like that, it would be great if you could open a pull request to add it.

[Wrenna Robson]

Sure, of course - I just wanted to check there wasn't some obvious reason we didn't have it!

[Wrenna Robson]

#26170