Unfold fail & LazyList nested induction issue

Stream: lean4

[James Gallicchio]

On further poking it looks like the second issue is because it tries to generalize h, but then the motive for the nested induction is left as a meta-variable and thus doesn't have the (h : _) -> binder it expects to have

[James Gallicchio]

which, actually, is still the case if h is moved into the return type:

theorem rotate_inv {F : LazyList α} {R} {S}
  : (h : _) → (rotate F R S h).toList = F.toList ++ R.reverse
  := by
  induction F
  case mk fn ih =>
    intro h
    exact ih ()
  repeat {sorry}

The intro raises the same error.

[James Gallicchio]

(Cleaned up the MWE above quite a bit; this seems to be as simple as I can get it)

[Leonardo de Moura]

Thanks for the MWE. I am working on it.