how to name an unnamed variable in cases statement

Stream: new members

[Becker A.]

I'm writing a proof where I use the cases tactic on a Nat; this splits the nat into two cases, where either it's 0 or strictly greater than 0. However for the latter case, it generates an unnamed variable for the new greater-than-zero nat, and I want to use it except I can't because it's unnamed.

e.g.:

example
  (n : ℕ)
  : ℕ
  := by
  cases n
  · exact 0
  -- <- here!

this generates the tactic state:

1 goal
case succ
n✝ : ℕ
⊢ ℕ

where n✝ is unnamed.

-> how do I use the unnamed n✝?

[Snir Broshi]

Well you can use tactics like expose_names and rename_i 0 to restore unaccessible names, but in this case you should just cases n with

[Snir Broshi]

import Mathlib
example (n : ℕ) : ℕ := by
  cases n with
  | zero => exact 0
  | succ n => sorry

[Snir Broshi]

You can also match n in term mode (if you delete the by, which is advisable when defining functions rather than theorems):

import Mathlib
example (n : ℕ) : ℕ :=
  match n with
  | .zero => 0
  | .succ n => sorry

[Kevin Buzzard]

Note that you can generate that boilerplate stuff by clicking on the yellow lightbulb that you can see in this screenshot

Screenshot from 2025-12-08 19-20-26.png

and then selecting "Generate an explicit pattern match"

[Becker A.]

this answers my question, thanks! feel free to resolve this topic