Theorem: Etch.Verification.Stream.IsMonotonic.imap (Etch/StreamFusion/Proofs/Imap.lean)

State before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
⊢ IsMonotonic (imap_general f g s)
Tactic:
rw [Stream.isMonotonic_iff]
State after:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
⊢ ∀ (q : { x // (imap_general f g s).valid x = true }) (i : Lex (ι' × Bool))
    (hq : (imap_general f g s).valid ((imap_general f g s).seek q i) = true),
    (imap_general f g s).index q ≤ (imap_general f g s).index { val := (imap_general f g s).seek q i, property := hq }

State before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
⊢ ∀ (q : { x // (imap_general f g s).valid x = true }) (i : Lex (ι' × Bool))
    (hq : (imap_general f g s).valid ((imap_general f g s).seek q i) = true),
    (imap_general f g s).index q ≤ (imap_general f g s).index { val := (imap_general f g s).seek q i, property := hq }
Tactic:
rintro q ⟨i, b⟩ hq
State after:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // (imap_general f g s).valid x = true }
i : ι'
b : Bool
hq : (imap_general f g s).valid ((imap_general f g s).seek q (i, b)) = true
⊢ (imap_general f g s).index q ≤
    (imap_general f g s).index { val := (imap_general f g s).seek q (i, b), property := hq }

State before:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // (imap_general f g s).valid x = true }
i : ι'
b : Bool
hq : (imap_general f g s).valid ((imap_general f g s).seek q (i, b)) = true
⊢ (imap_general f g s).index q ≤
    (imap_general f g s).index { val := (imap_general f g s).seek q (i, b), property := hq }
Tactic:
dsimp at q hq ⊢
State after:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ f (s.index q) ≤ f (s.index { val := s.seek q (g (s.index q) i, b), property := hq })

State before:
case mk
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ f (s.index q) ≤ f (s.index { val := s.seek q (g (s.index q) i, b), property := hq })
Tactic:
apply hf
State after:
case mk.a
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ s.index q ≤ s.index { val := s.seek q (g (s.index q) i, b), property := hq }

State before:
case mk.a
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
α : Type u_1
s : Stream ι α
hs : IsMonotonic s
f : ι → ι'
g : ι → ι' → ι
hf : Monotone f
q : { x // s.valid x = true }
i : ι'
b : Bool
hq : s.valid (s.seek q (g (s.index q) i, b)) = true
⊢ s.index q ≤ s.index { val := s.seek q (g (s.index q) i, b), property := hq }
Tactic:
apply Stream.isMonotonic_iff.mp hs q
State after:
no goals