Unaddressable names

Stream: new members

[Adam Langley]

Newly in Lean 4 (I think?) automatically-named values because unaddressable. (E.g. x:cross: in tactic mode.) How does one give them names, for example when using the induction tactic?

[Adam Langley]

(have : type := by assumption will find things by type, but it doesn't make sense when the type is Nat.)

[Moritz Doll]

For induction it is the with keyword: induction n with k hk,

[Adam Langley]

I tried induction ... with, but Lean 4 says unknown tactic.

[Adam Langley]

Ah, perhaps:
induction n with | zero => ... | succ n ih =>

[Adam Langley]

Hmm, split creates many unaddressable names too.

[Moritz Doll]

oh sorry I was thinking Lean 3

[Moritz Doll]

in Lean 4 you can use

example (n : ℕ) : n = n := by
  induction' n with k hk
  · sorry
  · sorry

[Adam Langley]

induction' gives unknown tactic for me. Is that part of math lib?

[Moritz Doll]

yes

[Moritz Doll]

ah the version you wrote seems to be prefered: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Cases.html

[Adam Langley]

Ah, thank you. Similar tricks don't seem to work with the unaddressable names coming from a split, however.

[Mario Carneiro]

for split, you can either use rename_i a b c or next a b c => to name the variables produced by the split