Theorem: Etch.Verification.Stream.min_toOrder_le (Etch/StreamFusion/Proofs/StreamZip.lean)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q)) ≤ toOrder (zip a b) q
Tactic:
rw [Prod.Lex.le_iff'']
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ≤ (toOrder (zip a b) q).1 ∧
    ((min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ≤ (toOrder (zip a b) q).1 ∧
    ((min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)
Tactic:
simp only [Monotone.map_min (@Prod.Lex.fst_mono ι Bool _ _)]
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1 ∧
    (min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1 ∧
    (min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)
Tactic:
constructor
State after:
case left
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1

case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
    (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2

State before:
case left
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1
Tactic:
exact min_le_max
State after:
no goals

State before:
case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
    (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2
Tactic:
simp only [toOrder]
State after:
case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (a.index (mul.valid.fst q)) (b.index (mul.valid.snd q)) = (zip a b).index q →
    (min (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 ≤
      (zip a b).ready q

State before:
case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (a.index (mul.valid.fst q)) (b.index (mul.valid.snd q)) = (zip a b).index q →
    (min (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 ≤
      (zip a b).ready q
Tactic:
aesop
State after:
no goals