α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), take n s ++ₛ drop n s = s
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), take n s ++ₛ drop n s = s
intro n
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), take zero s ++ₛ drop zero s = s

case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
⊢ ∀ (s : Stream' α), take (succ n') s ++ₛ drop (succ n') s = s
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), take n s ++ₛ drop n s = s
induction' n with n' ih
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ take zero s ++ₛ drop zero s = s
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), take zero s ++ₛ drop zero s = s
intro s
no goals
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ take zero s ++ₛ drop zero s = s
rfl
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
s : Stream' α
⊢ take (succ n') s ++ₛ drop (succ n') s = s
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
⊢ ∀ (s : Stream' α), take (succ n') s ++ₛ drop (succ n') s = s
intro s
no goals
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
s : Stream' α
⊢ take (succ n') s ++ₛ drop (succ n') s = s
rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]