α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = nth s₂ (succ n)
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (2 * (n + 1) + 1) = nth s₂ (n + 1)
change nth (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = nth s₂ (succ n)
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (tail s₂) n = nth s₂ (succ n)
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = nth s₂ (succ n)
rw [nth_succ, nth_succ, interleave_eq, tail_cons, tail_cons,
  nth_interleave_right n (tail s₁) (tail s₂)]
no goals
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (tail s₂) n = nth s₂ (succ n)
rfl