case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ ∀ (n : ℕ), nth (inits s) n = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) n
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ inits s = [head s] :: map (List.cons (head s)) (inits (tail s))
apply Stream'.ext
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ nth (inits s) n = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) n
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ ∀ (n : ℕ), nth (inits s) n = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) n
intro n
case a.zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ nth (inits s) zero = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) zero

case a.succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ nth (inits s) (succ n✝) = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) (succ n✝)
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ nth (inits s) n = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) n
cases n
no goals
case a.zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ nth (inits s) zero = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) zero
rfl
case a.succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ take (succ (succ n✝)) s = head s :: take (succ n✝) (tail s)
case a.succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ nth (inits s) (succ n✝) = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) (succ n✝)
rw [nth_inits, nth_succ, tail_cons, nth_map, nth_inits]
no goals
case a.succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ take (succ (succ n✝)) s = head s :: take (succ n✝) (tail s)
rfl