Induction hypothesis name

Stream: lean4

[Shreyas Srinivas]

Is there a way to fix the name of the induction hypothesis in advance for all cases so I can use it in the form
induction I <introduce IH name> <;> try {something_with_IH first}.

Also with the induction tactic what is the correct syntax for something like

induction x <;> {some tactics for covering many cases}
 | remaining case 1 var1 var2=> ...
 | remaining case 2 var1 var2 => ..

For this second question, I am using case <remaining case 1 name> <var_1> <var_2> => .... etc, but I recall that this is the style of the induction' tactic.

[Shreyas Srinivas]

I am aware of the induction' way of doing things, but I want to understand the induction tactic style of lean 4

[Mario Carneiro]

you can use induction x with (some tactics) | foo var1 var2 => ... | bar var1 var2 => ...

[Shreyas Srinivas]

And naming the IH?

[Shreyas Srinivas]

Basically I have one of those semantics proofs where a standard set of steps will close the inductive parts, if I have the name of the IH.

[Mario Carneiro]

yes you can name the IH, it just goes after the variables

[Mario Carneiro]

if you mean in (some tactics), no you will have to pick it up implicitly because there may be zero or more IHs in general. But most tactics have some way of doing this like simp [*] or assumption

[Shreyas Srinivas]

I do mean in the (some tactics) part.

[Shreyas Srinivas]

There is a specific point where I would like to rw[IH]

[Mario Carneiro]

simp only [*]?

[Mario Carneiro]

or rename_i IH; rw [IH] but there is no guarantee that you pick up the right variable this way

[Shreyas Srinivas]

Okay... In most of my proofs there is one inductive type, so there is either no IH or one IH

[Mario Carneiro]

the number of IHs depends on how many recursive arguments there are in the constructor

[Shreyas Srinivas]

Yeah that makes sense

[Shreyas Srinivas]

Rename_I doesn't do the trick because each branch has a different number of variables that need to be renamed before the IH comes up

[Mario Carneiro]

rename_i names variables right to left, so it should work unless you have multiple IHs

[Shreyas Srinivas]

the problem is it complains that there are too many variables in the base case