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

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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ 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 : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ 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 : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ 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:
exact max_le_max (ha _ _) (hb _ _)
State after:
no goals