Etch/StreamFusion/Proofs/StreamMul.lean:148:8: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression

[grue-bleen]

./././Etch/StreamFusion/Proofs/StreamMul.lean:148:8: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(evalMultiset a (a.seek (mul.valid.fst q) ((mul a b).index q, (mul a b).ready q))) j
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : ((mul a b).index q, (mul a b).ready q) ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) ((mul a b).index q, (mul a b).ready q))) j *
(eval b (b.seek (mul.valid.snd q) ((mul a b).index q, (mul a b).ready q))) j =
(eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j
./././Etch/StreamFusion/Proofs/StreamMul.lean:173:28: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(evalMultiset ?m.79551 (?m.79551.seek ?q ?i)) ?j
case e_a
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) i)) j = (eval a (↑q).1) j
./././Etch/StreamFusion/Proofs/StreamMul.lean:173:28: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(evalMultiset ?m.79652 (?m.79652.seek ?q ?i)) ?j
case e_a
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
⊢ (eval b (b.seek (mul.valid.snd q) i)) j = (eval b (↑q).2) j
./././Etch/StreamFusion/Proofs/StreamMul.lean:173:52: warning: aesop: failed to prove the goal after exhaustive search.
./././Etch/StreamFusion/Proofs/StreamMul.lean:173:52: warning: aesop: failed to prove the goal after exhaustive search.
./././Etch/StreamFusion/Proofs/StreamMul.lean:171:66: error: unsolved goals
ι : Type
inst : LinearOrder ι
α : Type u
inst_1 : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst_2 : IsStrictLawful a
inst_3 : IsStrictLawful b
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
val : (mul a b).σ
property : (mul a b).valid val = true
⊢ (eval a (a.seek (mul.valid.fst { val := val, property := property }) i)) j = (eval a val.1) j

ι : Type
inst : LinearOrder ι
α : Type u
inst_1 : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst_2 : IsStrictLawful a
inst_3 : IsStrictLawful b
i : Lex (ι × Bool)
j : ι
h : i ≤ (j, false)
val : (mul a b).σ
property : (mul a b).valid val = true
⊢ (eval b (b.seek (mul.valid.snd { val := val, property := property }) i)) j = (eval b val.2) j
./././Etch/StreamFusion/Proofs/StreamMul.lean:177:15: error: type mismatch
mul_seek_spec a b
has type
∀ (q : { q // (mul a b).valid q = true }) (i : Lex (ι × Bool)) (j : ι),
i ≤ (j, false) → (eval (mul a b) ((mul a b).seek q i)) j = (eval (mul a b) ↑q) j : Prop
but is expected to have type
∀ (q : { x // (mul a b).valid x = true }) (i : StreamOrder ι) (j : ι),
i ≤ (j, false) → (evalMultiset (mul a b) ((mul a b).seek q i)) j = (evalMultiset (mul a b) ↑q) j : Prop