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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
⊢ index' (mul a b) ↑q < index' (mul a b) ((mul a b).seek q i)
Tactic:
simp only [Stream.mul_index']
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Tactic:
have := order_eq_of_mul_ready hr
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Tactic:
simp at hr
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
hr :
  (a.ready (mul.valid.fst q) = true ∧ b.ready (mul.valid.snd q) = true) ∧
    a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
hr :
  (a.ready (mul.valid.fst q) = true ∧ b.ready (mul.valid.snd q) = true) ∧
    a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Tactic:
apply max_lt_max (ha.lt (hr := hr.1.1) ..) (hb.lt (hr := hr.1.2) ..) <;>
  simpa [this]
State after:
no goals