α : Type u
β : Type v
δ : Type w
a : α
n : ℕ
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n = nth (initsCore (a :: l) s) n
α : Type u
β : Type v
δ : Type w
⊢ ∀ (a : α) (n : ℕ) (l : List α) (s : Stream' α), a :: nth (initsCore l s) n = nth (initsCore (a :: l) s) n
intro a n
case zero
α : Type u
β : Type v
δ : Type w
a : α
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) zero = nth (initsCore (a :: l) s) zero

case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) (succ n') = nth (initsCore (a :: l) s) (succ n')
α : Type u
β : Type v
δ : Type w
a : α
n : ℕ
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n = nth (initsCore (a :: l) s) n
induction' n with n' ih
case zero
α : Type u
β : Type v
δ : Type w
a : α
l✝ : List α
s✝ : Stream' α
⊢ a :: nth (initsCore l✝ s✝) zero = nth (initsCore (a :: l✝) s✝) zero
case zero
α : Type u
β : Type v
δ : Type w
a : α
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) zero = nth (initsCore (a :: l) s) zero
intros
no goals
case zero
α : Type u
β : Type v
δ : Type w
a : α
l✝ : List α
s✝ : Stream' α
⊢ a :: nth (initsCore l✝ s✝) zero = nth (initsCore (a :: l✝) s✝) zero
rfl
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
l : List α
s : Stream' α
⊢ a :: nth (initsCore l s) (succ n') = nth (initsCore (a :: l) s) (succ n')
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) (succ n') = nth (initsCore (a :: l) s) (succ n')
intro l s
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
l : List α
s : Stream' α
⊢ nth (initsCore (a :: (l ++ [head s])) (tail s)) n' =
    nth ((a :: l) :: initsCore (a :: l ++ [head s]) (tail s)) (succ n')
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
l : List α
s : Stream' α
⊢ a :: nth (initsCore l s) (succ n') = nth (initsCore (a :: l) s) (succ n')
rw [nth_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a::l) s]
no goals
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
l : List α
s : Stream' α
⊢ nth (initsCore (a :: (l ++ [head s])) (tail s)) n' =
    nth ((a :: l) :: initsCore (a :: l ++ [head s]) (tail s)) (succ n')
rfl