Unfold fails

Stream: lean4

[James Gallicchio]

Found an example that causes unfold to fail:

inductive LazyList (α : Type u)
| nil : LazyList α
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk (LazyList α)) : LazyList α

namespace LazyList
def length : LazyList α → Nat
| nil        => 0
| cons _ as  => length as + 1
| delayed as => length as.get

def force : LazyList α → Option (α × LazyList α)
| delayed as => force as.get
| nil        => none
| cons a as  => some (a,as)

def toList : LazyList α → List α
| nil        => []
| cons a as  => a :: toList as
| delayed as => toList as.get
end LazyList

structure RTQueue (τ) :=
  F : LazyList τ
  R : List τ
  S : LazyList τ
  h_lens : F.length = R.length + S.length

namespace RTQueue

def empty : RTQueue τ :=
  ⟨ LazyList.nil,
    List.nil,
    LazyList.nil,
    by simp
  ⟩

@[inline] def rotate (f : LazyList τ) (r : List τ) (a : LazyList τ)
  (h : f.length + 1 = r.length) : LazyList τ :=
  LazyList.delayed (
    match h_r:r with
    | List.nil => sorry
    | y::r' =>
    match h_f:f.force with
    | none => LazyList.cons y a
    | some (x, f') => LazyList.cons x (rotate f' r' (LazyList.cons y a) (sorry))
  )

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

The issue goes away if rotate doesn't take the h parameter, OR if there is only one match instead of two. So I'm not sure how to cut down this MWE more.

[James Gallicchio]

And a minor error-message complaint, I originally wrote rotate_inv as

theorem rotate_inv {F : LazyList α} {R} {S} (h)
  : (rotate F R S h).toList = F.toList ++ R.reverse
  := by
    induction F
    repeat {sorry}

with the h as a parameter, and got a nebulous tactic 'introN' failed, insufficient number of binders at induction F. Unsure if that is an issue or if the error message is just too generic.