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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ toOrder (mul a b) q ≤ max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))
Tactic:
rw [Prod.Lex.le_iff']
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 < (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∨
    (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
      (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 < (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∨
    (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
      (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
right
State after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
    (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2

State before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
    (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
constructor
State after:
case h.left
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1

case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2

State before:
case h.left
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1
Tactic:
simp [Monotone.map_max (@Prod.Lex.fst_mono ι Bool _ _)]
State after:
no goals

State before:
case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (toOrder (mul a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
simp only [Bool.le_iff_imp, toOrder]
State after:
case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (mul a b).ready q = true →
    (max (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 =
      true

State before:
case h.right
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (mul a b).ready q = true →
    (max (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 =
      true
Tactic:
aesop
State after:
no goals