case zero
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
h : some a = Stream'.nth (↑(think s)) Nat.zero
⊢ a ∈ s

case succ
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n' : ℕ
h : some a = Stream'.nth (↑(think s)) (Nat.succ n')
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : (fun b => some a = b) (Stream'.nth (↑(think s)) n)
⊢ a ∈ s
cases' n with n'
case succ
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n' : ℕ
h : some a = Stream'.nth (↑(think s)) (Nat.succ n')
⊢ a ∈ s
case zero
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
h : some a = Stream'.nth (↑(think s)) Nat.zero
⊢ a ∈ s

case succ
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n' : ℕ
h : some a = Stream'.nth (↑(think s)) (Nat.succ n')
⊢ a ∈ s
contradiction
no goals
case succ
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n' : ℕ
h : some a = Stream'.nth (↑(think s)) (Nat.succ n')
⊢ a ∈ s
exact ⟨n', h⟩