Giving names to 'cases' variables

Stream: new members

[Nir Paz]

How can I give names to the variables introduced by 'cases' when it's run on a type with recursive constructors? I can see in the documentation that you can pass a list of names, but I can't figure out how to write that in code.

Also, is there a way to rename/access :cross:-variables? Although that seems like a bad way to solve this problem anyways.

[Martin Dvořák]

Are you using Lean 3 or Lean 4 now?

[Patrick Massot]

Martin, the tombstone symbol means Lean 4.

[Patrick Massot]

Nir Paz, it will be a lot easier to help you if you post a #mwe

[Martin Dvořák]

It just seemed a bit that @Nir Paz had documentation for Lean 3.

[Damiano Testa]

Btw, the "bad way" is rename_i a b c ..., but I share the sentiment.

[Ruben Van de Velde]

I suspect you're looking for cases xxx with | foo a b c => proof

[Ruben Van de Velde]

If you write cases foo, there should be a :light_bulb: icon in Vs code that you can click to generate the rest. You may need some mathlib imports

[Kyle Miller]

There's also

next a b c =>
  proof

to rename and focus on the next goal

[Nir Paz]

@Martin Dvořák Oh, I think I was looking at mathlib3 documentation (is this mathlib3? https://leanprover-community.github.io/mathlib_docs/index.html). Once I found the mathlib4 docs I found what I needed, just using cases' instead.

[Nir Paz]

It's too bad that's the first result on google

[Ruben Van de Velde]

Yeah, we've only just transitioned to lean 4, it'll take a while to clean everything up

[Patrick Massot]

We need to add a big deprecation banner to https://leanprover-community.github.io/mathlib_docs/index.html. @Rob Lewis?

[Eric Wieser]

https://github.com/leanprover-community/doc-gen/pull/178 does the slightly lower effort path of adding 3s in a handful of places