induction' i with i ih generalizing j σ
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
case zero
α : Type u_1
σ✝ : Stream' α
j✝ : ℕ
σ : Stream' α
j : ℕ
⊢ (take Nat.zero σ ++ take j fun i => σ (i + Nat.zero)) = take (Nat.zero + j) σ

case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take (Nat.succ i) σ ++ take j fun i_1 => σ (i_1 + Nat.succ i)) = take (Nat.succ i + j) σ