Auto-filling fields of a structure

Stream: new members

[Stuart Presnell]

If I'm about to define a structure (e.g. an equiv) is there some clever trick I can do to auto-fill the fields

{
to_fun    := sorry,
inv_fun   := sorry,
left_inv  := sorry,
right_inv := sorry,
}

[Johan Commelin]

write _, and click on the :bulb: then select the item containing "skeleton"

[Johan Commelin]

I think Ctrl+. is a shortcut for the :bulb:

[Johan Commelin]

def my_equiv : α ≃ β :=
_ -- put your cursor on the `_`

[Stuart Presnell]

Magic! Thank you!