Theorem: Etch.Verification.IsBounded.mk' (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
h :
  ∃ wf_rel,
    ∀ (q : s.σ) (i : StreamOrder ι),
      WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (s.seek q i) ↑q ∨ i < Stream.toOrder s q ∧ s.seek q i = ↑q
Tactic:
simp only [wf_valid_iff]
State after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
h :
  ∃ wf_rel,
    ∀ (q : s.σ) (i : StreamOrder ι),
      WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
h :
  ∃ wf_rel,
    ∀ (q : s.σ) (i : StreamOrder ι),
      WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Tactic:
rcases h with ⟨wfr, hr⟩
State after:
case intro
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
wfr : WellFoundedRelation s.σ
hr :
  ∀ (q : s.σ) (i : StreamOrder ι),
    WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q

State before:
case intro
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : Preorder ι
wfr : WellFoundedRelation s.σ
hr :
  ∀ (q : s.σ) (i : StreamOrder ι),
    WellFoundedRelation.rel (Stream.seek' s q i) q ∨ coeLex i < Stream.toOrder' s q ∧ Stream.seek' s q i = q
⊢ ∃ wf_rel,
    ∀ (q : { x // s.valid x = true }) (i : Lex (ι × Bool)),
      WellFoundedRelation.rel (Stream.seek' s (↑q) i) ↑q ∨ coeLex i < Stream.toOrder' s ↑q ∧ Stream.seek' s (↑q) i = ↑q
Tactic:
exact ⟨wfr, fun q i => hr q i⟩
State after:
no goals