How to make induction tactic produce equality?

Stream: lean4

[Andrey Yao]

Say I have a list l and I want to do induction l with | nil => ... | cons hd tl IH => ..., how do I get Lean to produce the hypothesis l = cons hd tl in the second case? It would be similar to the induction ... eqn:E tactic from Coq, Thanks!

[Kyle Miller]

This feature doesn't exist yet for induction. If you use mathlib, induction' h : l would work, but then you don't get the with syntax. (For induction', the with clause takes a list of all the variable names. It's like in the Lean 3 version of induction.)

[Kyle Miller]

I think this simulates it:

example (p : List Nat → Prop) (l : List Nat) : p l := by
  generalize h : l = l'
  induction l' generalizing l with
  | nil => sorry
  | cons hd tl IH => sorry

[Andrey Yao]

That worked! Tysm