α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
⊢ Option.map (fun a' => (a', tail s)) (get? s 0) = some (a, s') → s = cons a s'
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
⊢ destruct s = some (a, s') → s = cons a s'
dsimp [destruct]
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = some (a, s')
⊢ s = cons a s'

case some
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
a' : α
f0 : get? s 0 = some a'
h : Option.map (fun a' => (a', tail s)) (some a') = some (a, s')
⊢ s = cons a s'
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
⊢ Option.map (fun a' => (a', tail s)) (get? s 0) = some (a, s') → s = cons a s'
induction' f0 : get? s 0 with a' <;> intro h
no goals
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = some (a, s')
⊢ s = cons a s'
contradiction
case some.mk
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h : Option.map (fun a' => (a', tail { val := f, property := al })) (some a') = some (a, s')
⊢ { val := f, property := al } = cons a s'
case some
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
s' : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
a' : α
f0 : get? s 0 = some a'
h : Option.map (fun a' => (a', tail s)) (some a') = some (a, s')
⊢ s = cons a s'
cases' s with f al
case some.mk
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ { val := f, property := al } = cons a s'
case some.mk
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h : Option.map (fun a' => (a', tail { val := f, property := al })) (some a') = some (a, s')
⊢ { val := f, property := al } = cons a s'
injections _ h1 h2
case some.mk
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ { val := f, property := al } = cons a (tail { val := f, property := al })
case some.mk
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ { val := f, property := al } = cons a s'
rw [← h2]
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ ↑{ val := f, property := al } = ↑(cons a (tail { val := f, property := al }))
case some.mk
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ { val := f, property := al } = cons a (tail { val := f, property := al })
apply Subtype.eq
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ f = some a :: Stream'.tail f
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ ↑{ val := f, property := al } = ↑(cons a (tail { val := f, property := al }))
dsimp [tail, cons]
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ f = some a :: Stream'.tail f
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a'
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ f = some a :: Stream'.tail f
rw [h1] at f0
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ f = get? { val := f, property := al } 0 :: Stream'.tail f
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ f = some a :: Stream'.tail f
rw [← f0]
no goals
case some.mk.a
α : Type u
β : Type v
γ : Type w
a : α
s' : Seq α
x✝ : Option α
a' : α
f : Stream' (Option α)
al : IsSeq f
f0✝ : get? { val := f, property := al } 0 = x✝
f0 : get? { val := f, property := al } 0 = some a
h1 : a' = a
h2 : tail { val := f, property := al } = s'
⊢ f = get? { val := f, property := al } 0 :: Stream'.tail f
exact (Stream'.eta f).symm