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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
⊢ IsMonotonic (zip a b)
Tactic:
intro q i
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ index' (zip a b) ↑q ≤ index' (zip a b) ((zip a b).seek q i)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ index' (zip a b) ↑q ≤ index' (zip a b) ((zip a b).seek q i)
Tactic:
simp only [zip_index']
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ max (index' a (↑q).1) (index' b (↑q).2) ≤ max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ max (index' a (↑q).1) (index' b (↑q).2) ≤ max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)
Tactic:
exact max_le_max (ha _ _) (hb _ _)
State after:
no goals