Etch/StreamFusion/Proofs/Imap.lean:60:4: error: tactic 'apply' failed, failed to unify

[grue-bleen]

./././Etch/StreamFusion/Proofs/Imap.lean:60:4: error: tactic 'apply' failed, failed to unify
(evalMultiset s (s.seek ?q ?i)) ?j = (evalMultiset s ↑?q) ?j
with
(eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i
case pos
ι ι' : Type
inst✝³ : LinearOrder ι
inst✝² : LinearOrder ι'
α : Type u_1
s : Stream ι α
inst✝¹ : AddZeroClass α
inst✝ : IsLawful s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
hg : ∀ (j : ι'), Monotone fun x => g x j
hfg : ∀ (i : ι) (j : ι'), compareOfLessAndEq j (f i) = compareOfLessAndEq (g i j) i
this : IsBounded (imap_general f g s)
q : { x // s.valid x = true }
j₁ : ι'
b : Bool
i : ι
hj : (j₁, b) ≤ (f i, false)
le : s.index q ≤ i
⊢ (eval s (s.seek q (g (s.index q) j₁, b))) i = (eval s ↑q) i