Theorem: Etch.Verification.Stream.mul_seek_spec (Etch/StreamFusion/Proofs/StreamMul.lean)

State before:
ι : 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 (mul a b) ((mul a b).seek q i)) j = (eval (mul a b) ↑q) j
Tactic:
simp only [Finsupp.mul_apply, mul_spec]
State after:
ι : 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 ((mul a b).seek q i).1) j * (eval b ((mul a b).seek q i).2) j = (eval a (↑q).1) j * (eval b (↑q).2) j

State before:
ι : 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 ((mul a b).seek q i).1) j * (eval b ((mul a b).seek q i).2) j = (eval a (↑q).1) j * (eval b (↑q).2) j
Tactic:
congr 1 <;> dsimp <;> rw [IsLawful.seek_spec] <;> aesop
State after:
ι : 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