rename inaccessibles with pattern

Stream: lean4

[Iason Marmanis]

I end up with some inaccessible terms of type X in my context.
Is there a way to do something like rename X => x for both of them, and have e.g. x1 : X, x2 : X?

[Kenny Lau]

@Iason Marmanis https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.exposeNames

[Iason Marmanis]

thanks! but I was hoping for something more controlled (specific pattern/type with specific name)

[Aaron Liu]

Well there's also rename_i

[Aaron Liu]

it's probably better to do it so that you don't end up with inaccessible names in the first place, though

[Iason Marmanis]

yeah, that's what i'm doing now but I just find it cumbersome to name them in order.
I get e.g. 10 inaccessible in one go and when I start naming them the names move around (screen order) and it gets confusing

[Kevin Buzzard]

Can you un-#xy ? As Aaron said, rename_i is a solution, but this is rarely if ever used in e.g. mathlib, so maybe what you're doing is unidiomatic.