case zero
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = nth (b :: s) zero
⊢ a = b ∨ a ∈ s

case succ
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth (b :: s) (succ n')
⊢ a = b ∨ a ∈ s
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n : ℕ
h : (fun b => a = b) (nth (b :: s) n)
⊢ a = b ∨ a ∈ s
cases' n with n'
case zero.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = nth (b :: s) zero
⊢ a = b
case zero
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = nth (b :: s) zero
⊢ a = b ∨ a ∈ s
left
no goals
case zero.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = nth (b :: s) zero
⊢ a = b
exact h
case succ.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth (b :: s) (succ n')
⊢ a ∈ s
case succ
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth (b :: s) (succ n')
⊢ a = b ∨ a ∈ s
right
case succ.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth s n'
⊢ a ∈ s
case succ.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth (b :: s) (succ n')
⊢ a ∈ s
rw [nth_succ, tail_cons] at h
no goals
case succ.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth s n'
⊢ a ∈ s
exact ⟨n', h⟩