Finding constructors

Stream: new members

[Nathan]

Where can I find the constructor for Equiv.Perm?

[Ruben Van de Velde]

docs#Equiv.Perm

[Notification Bot]

A message was moved here from #new members > mvcgen doesn't produce any invariant goals by Ruben Van de Velde.

[Nathan]

I don't get it, which part shows the constructor?

[Ruben Van de Velde]

Depends on what you mean by "constructor"

[Ruben Van de Velde]

That shows it's an abbrev, and if you click "Equations" it shows (α ≃ α), so you need to construct it as if it was a docs#Equiv

[Nathan]

so i need two functions and a proof of left inverse and a proof of right inverse?

[Ruben Van de Velde]

Yep

[Kevin Buzzard]

Screenshot 2025-09-29 at 13.01.18.png

(screenshot didn't capture it but my cursor was just before the s of sorry)

and then click on the blue lightbulb, select "generate a skeleton..." and you get

import Mathlib

def e : Equiv.Perm ℕ where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

[Nathan]

oh perfect, thanks