Theorem: Stream'.take_succ_to_concat (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take (i + 1) σ = List.concat (take i σ) (σ i)
Tactic:
rw [←take_append_drop_take]
State after:
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take i σ ++ take 1 (drop i σ) = List.concat (take i σ) (σ i)

State before:
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take i σ ++ take 1 (drop i σ) = List.concat (take i σ) (σ i)
Tactic:
simp only [take, head, nth, drop, zero_add, List.concat_eq_append]
State after:
no goals