α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ tail s
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
⊢ a ∈ tail s → a ∈ s
intro h
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h this : a ∈ tail s
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : a ∈ tail s
⊢ a ∈ s
have := h
case intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
this : a ∈ tail s
n : ℕ
e : (fun b => some (some a) = b) (nth (↑(tail s)) n)
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h this : a ∈ tail s
⊢ a ∈ s
cases' h with n e
case intro
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ tail s → (fun b => some (some a) = b) (nth (↑(tail s)) n) → a ∈ s
case intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
this : a ∈ tail s
n : ℕ
e : (fun b => some (some a) = b) (nth (↑(tail s)) n)
⊢ a ∈ s
revert s
case intro
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
case intro
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ tail s → (fun b => some (some a) = b) (nth (↑(tail s)) n) → a ∈ s
simp [Stream'.nth]
case intro.zero.h2
α : Type u
β : Type v
γ : Type w
a x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s 0
⊢ a = x ∨ a ∈ s

case intro.succ.h2
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s (Nat.succ n)
⊢ a = x ∨ a ∈ s

case intro.succ.h3
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
⊢ a ∈ s
case intro
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
induction' n with n IH <;> intro s <;> induction' s using WSeq.recOn with x s s <;>
  simp <;> intro m e <;>
  injections
no goals
case intro.zero.h2
α : Type u
β : Type v
γ : Type w
a x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s 0
⊢ a = x ∨ a ∈ s
exact Or.inr m
no goals
case intro.succ.h2
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
x : α
s : WSeq α
m : a ∈ s
e : some (some a) = ↑s (Nat.succ n)
⊢ a = x ∨ a ∈ s
exact Or.inr m
case intro.succ.h3
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
⊢ some (some a) = ↑(tail s) n
case intro.succ.h3
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
⊢ a ∈ s
apply IH m
case intro.succ.h3
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
⊢ ↑(think (tail s)) (Nat.succ n) = ↑(tail s) n
case intro.succ.h3
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
⊢ some (some a) = ↑(tail s) n
rw [e]
case intro.succ.h3.mk
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
val✝ : Stream' (Option (Option α))
property✝ : IsSeq val✝
⊢ ↑(think { val := val✝, property := property✝ }) (Nat.succ n) = ↑{ val := val✝, property := property✝ } n
case intro.succ.h3
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
⊢ ↑(think (tail s)) (Nat.succ n) = ↑(tail s) n
cases tail s
no goals
case intro.succ.h3.mk
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, a ∈ tail s → some (some a) = ↑(tail s) n → a ∈ s
s : WSeq α
m : a ∈ tail s
e : some (some a) = ↑(think (tail s)) (Nat.succ n)
val✝ : Stream' (Option (Option α))
property✝ : IsSeq val✝
⊢ ↑(think { val := val✝, property := property✝ }) (Nat.succ n) = ↑{ val := val✝, property := property✝ } n
rfl