How can I get the equation of a case in my context?

Stream: lean4

[Alex Zani]

So, for instance, I have

induction sizeOf state with
  | zero =>

I now would like to use the fact that sizeOf state = 0. But as far as I can tell, lean doesn't give me access to that. It replaces sizeOf state with 0 in the goal, but that doesn't let me manipulate instances of sizeOf state that are in my context.

[Aaron Liu]

simp knows about these lemmas

[Aaron Liu]

Do induction h : sizeOf state with

[Alex Zani]

Aaron Liu said:

Do induction h : sizeOf state with

I get unknown identifier h.

[Aaron Liu]

What version of Lean are you on?

[Alex Zani]

4.10

[Aaron Liu]

Try generalize sizeOf state = x and then induction x generalizing state with

[Alex Zani]

Aaron Liu said:

Try generalize sizeOf state = x and then induction x generalizing state with

x is not in the proof state unfortunately.

[Alex Zani]

Neither is sizeOf state = 0

[Aaron Liu]

Alex Zani said:

Aaron Liu said:

Try generalize sizeOf state = x and then induction x generalizing state with

x is not in the proof state unfortunately.

generalize should add x to the proof state? If it doesn't then that's a bug.

[Alex Zani]

It does. But it looks like it's removed in the induction cases.

[Aaron Liu]

Oh, that should be generalize h : sizeOf state = x

[Alex Zani]

Aaron Liu said:

Oh, that should be generalize h : sizeOf state = x

Thanks, that worked!