α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (inits s) n = take (succ n) s
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), nth (inits s) n = take (succ n) s
intro n
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (inits s) zero = take (succ zero) s

case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (inits s) n' = take (succ n') s
⊢ ∀ (s : Stream' α), nth (inits s) (succ n') = take (succ (succ n')) s
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (inits s) n = take (succ n) s
induction' n with n' ih
case zero
α : Type u
β : Type v
δ : Type w
s✝ : Stream' α
⊢ nth (inits s✝) zero = take (succ zero) s✝
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (inits s) zero = take (succ zero) s
intros
no goals
case zero
α : Type u
β : Type v
δ : Type w
s✝ : Stream' α
⊢ nth (inits s✝) zero = take (succ zero) s✝
rfl
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (inits s) n' = take (succ n') s
s✝ : Stream' α
⊢ nth (inits s✝) (succ n') = take (succ (succ n')) s✝
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (inits s) n' = take (succ n') s
⊢ ∀ (s : Stream' α), nth (inits s) (succ n') = take (succ (succ n')) s
intros
no goals
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (inits s) n' = take (succ n') s
s✝ : Stream' α
⊢ nth (inits s✝) (succ n') = take (succ (succ n')) s✝
rw [nth_succ, take_succ, ← ih, tail_inits, inits_tail, cons_nth_inits_core]