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

State before:
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ take i σ ++ take j (drop i σ) = take (i + j) σ
Tactic:
simp only [drop, nth]
State after:
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ

State before:
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
Tactic:
induction' i with i ih generalizing j σ
State after:
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) σ

State before:
case zero
α : Type u_1
σ✝ : Stream' α
j✝ : ℕ
σ : Stream' α
j : ℕ
⊢ (take Nat.zero σ ++ take j fun i => σ (i + Nat.zero)) = take (Nat.zero + j) σ
Tactic:
simp [take]
State after:
no goals

State before:
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) σ
Tactic:
rw [Nat.add_assoc i 1 j, Nat.add_comm 1 j, ←Nat.add_assoc i j 1]
State after:
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) σ

State before:
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) σ
Tactic:
simp [take, ←ih]
State after:
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)

State before:
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)
Tactic:
congr
State after:
no goals