α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) n = nth s n
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), nth (unfolds head tail s) n = nth s n
intro n
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) zero = nth s zero

case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (unfolds head tail s) n' = nth s n'
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) (succ n') = nth s (succ n')
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) n = nth s n
induction' n with n' ih
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ nth (unfolds head tail s) zero = nth s zero
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) zero = nth s zero
intro s
no goals
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ nth (unfolds head tail s) zero = nth s zero
rfl
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (unfolds head tail s) n' = nth s n'
s : Stream' α
⊢ nth (unfolds head tail s) (succ n') = nth s (succ n')
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (unfolds head tail s) n' = nth s n'
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) (succ n') = nth s (succ n')
intro s
no goals
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (unfolds head tail s) n' = nth s n'
s : Stream' α
⊢ nth (unfolds head tail s) (succ n') = nth s (succ n')
rw [nth_succ, nth_succ, unfolds_eq, tail_cons, ih]