induction with fixed index

Stream: lean4

[Chris B]

What is the recommended way to do induction on a hypothesis that's an inductive Prop with an index fixed/not a variable? This seems to be a hard error in lean 4 (index in target's type is not a variable (consider using the cases tactic instead)).

Right now I'm doing this to keep the (c = ..) lemma out of the signature:

theorem bigStepWhileDiverges
  {body s0 s1}
  (h0 : BigStep (while (fun _ => True) body) s0 s1)
  : False :=
by
generalize hc : (while (fun _ => True) body) = c
rw [hc] at h0
induction h0 with
...

where BigStep is all indices: inductive BigStep : Stmt -> State -> State -> Prop

[Mario Carneiro]

The standard way to work around this in lean 3 is to generalize the fixed index and add an equality hypothesis. This can be done by generalize in lean 3, which I believe also exists in lean 4, but if it doesn't work you can also use suffices and do it manually

[Mario Carneiro]

your code suggests you already know this trick, which would be only improved by incorporating the improved generalize_hyp mathlib tactic (which is a straight generalization of generalize to allow generalizing at hypotheses too)