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

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