Theorem: Etch.Verification.Stream.next_eval_mul_eq (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 }
⊢ eval a (advance (mul a b) ↑q).1 * eval b (advance (mul a b) ↑q).2 =
    Finsupp.filter (fun i => toOrder (mul a b) q ≤ (i, false)) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
ext j
State after:
case h
ι : 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 : ι
⊢ (eval a (advance (mul a b) ↑q).1 * eval b (advance (mul a b) ↑q).2) j =
    (Finsupp.filter (fun i => toOrder (mul a b) q ≤ (i, false)) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)))
      j

State before:
case h
ι : 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 : ι
⊢ (eval a (advance (mul a b) ↑q).1 * eval b (advance (mul a b) ↑q).2) j =
    (Finsupp.filter (fun i => toOrder (mul a b) q ≤ (i, false)) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)))
      j
Tactic:
simp only [Finsupp.mul_apply, Finsupp.filter_apply, Stream.advance_val]
State after:
case h
ι : 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 : ι
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    if toOrder (mul a b) q ≤ (j, false) then (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j else 0

State before:
case h
ι : 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 : ι
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    if toOrder (mul a b) q ≤ (j, false) then (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j else 0
Tactic:
split_ifs with hj
State after:
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 : toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j

case neg
ι : 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 : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j = 0

State before:
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 : toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j
Tactic:
simp only [Stream.toOrder, Stream.index'_val, Stream.mul_seek] at hj ⊢
State after:
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

State before:
case neg
ι : 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 : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j = 0
Tactic:
dsimp only [mul_seek]
State after:
case neg
ι : 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 : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0

State before:
case neg
ι : 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 : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rw [not_le] at hj
State after:
case neg
ι : 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 : (j, false) < toOrder (mul a b) q
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0

State before:
case neg
ι : 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 : (j, false) < toOrder (mul a b) q
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rcases le_max_iff.mp <| toOrder_le_max a b q with hj' | hj'
State after:
case neg.inl
ι : 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 : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder a (mul.valid.fst q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0

case neg.inr
ι : 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 : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder b (mul.valid.snd q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0

State before:
case neg.inl
ι : 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 : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder a (mul.valid.fst q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rw [a.strictMono.eval_seek_eq_zero, MulZeroClass.zero_mul] <;> assumption
State after:
no goals

State before:
case neg.inr
ι : 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 : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder b (mul.valid.snd q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rw [b.strictMono.eval_seek_eq_zero, MulZeroClass.mul_zero] <;> assumption
State after:
no goals