simp [take, ←ih]
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 (i + j + 1) σ
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 j fun i_1 => σ (i_1 + Nat.succ i)) = take j fun i_1 => tail σ (i_1 + i)