Theorem: Etch.Verification.Stream.mul_eval₀_of_neq (Etch/StreamFusion/Proofs/StreamMul.lean)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : toOrder a (mul.valid.fst q) ≠ toOrder b (mul.valid.snd q)
⊢ eval₀ (mul a b) q = 0
Tactic:
contrapose! h
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ toOrder a (mul.valid.fst q) = toOrder b (mul.valid.snd q)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ toOrder a (mul.valid.fst q) = toOrder b (mul.valid.snd q)
Tactic:
apply Stream.mul.ready.order_eq
State after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ mul.ready a b q = true

State before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ mul.ready a b q = true
Tactic:
simp only [Stream.eval₀, Stream.mul_ready, Stream.mul_index, ge_iff_le, Stream.mul_value, ne_eq, dite_eq_right_iff,
  Finsupp.single_eq_zero, not_forall] at h
State after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h :
  ∃ (x :
    (a.ready (mul.valid.fst q) && b.ready (mul.valid.snd q) &&
        decide (a.index (mul.valid.fst q) = b.index (mul.valid.snd q))) =
      true),
    ¬a.value (mul.ready.fst { val := q, property := ⋯ }) * b.value (mul.ready.snd { val := q, property := ⋯ }) = 0
⊢ mul.ready a b q = true

State before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h :
  ∃ (x :
    (a.ready (mul.valid.fst q) && b.ready (mul.valid.snd q) &&
        decide (a.index (mul.valid.fst q) = b.index (mul.valid.snd q))) =
      true),
    ¬a.value (mul.ready.fst { val := q, property := ⋯ }) * b.value (mul.ready.snd { val := q, property := ⋯ }) = 0
⊢ mul.ready a b q = true
Tactic:
exact h.fst
State after:
no goals