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