Theorem: Etch.Verification.Stream.get_index' (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type ?u.13400
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
⊢ s.valid x = true
Tactic:
simpa using h
State after:
no goals

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
⊢ Option.get (index' s x) h = s.index { val := x, property := ⋯ }
Tactic:
generalize_proofs hq
State after:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
hq : s.valid x = true
⊢ Option.get (index' s x) h = s.index { val := x, property := hq }

State before:
ι : Type
α : Type u_1
a b s : Stream ι α
inst✝ : PartialOrder ι
x : s.σ
h : Option.isSome (index' s x) = true
hq : s.valid x = true
⊢ Option.get (index' s x) h = s.index { val := x, property := hq }
Tactic:
simp_rw [Stream.index', hq, Option.get]
State after:
no goals