[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
i : ℕ
⊢ (head s :: tail s) i = s i
[PROOFSTEP]
cases i
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ (head s :: tail s) zero = s zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ (head s :: tail s) (succ n✝) = s (succ n✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
n m : ℕ
s : Stream' α
⊢ drop n (drop m s) = drop (n + m) s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
n m : ℕ
s : Stream' α
n✝ : ℕ
⊢ nth (drop n (drop m s)) n✝ = nth (drop (n + m) s) n✝
[PROOFSTEP]
simp [Nat.add_assoc]
[GOAL]
α : Type u
β : Type v
δ : Type w
i : ℕ
s : Stream' α
⊢ tail (drop i s) = drop (i + 1) s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
i : ℕ
s : Stream' α
n✝ : ℕ
⊢ nth (tail (drop i s)) n✝ = nth (drop (i + 1) s) n✝
[PROOFSTEP]
simp [add_comm, add_assoc, add_left_comm]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ tail (drop n s) = drop n (tail s)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
δ : Type w
a : Stream' α
n : ℕ
⊢ head (drop n a) = nth a n
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
δ : Type w
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ x = y
[PROOFSTEP]
rw [← nth_zero_cons x s, h, nth_zero_cons]
[GOAL]
α : Type u
β : Type v
δ : Type w
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ nth s n = nth t n
[PROOFSTEP]
rw [← nth_succ_cons n _ x, h, nth_succ_cons]
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
s : Stream' α
b : α
x✝ : a ∈ s
n : ℕ
h : (fun b => a = b) (nth s n)
⊢ (fun b => a = b) (nth (b :: s) (succ n))
[PROOFSTEP]
rw [nth_succ, tail_cons, h]
[GOAL]
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n : ℕ
h : (fun b => a = b) (nth (b :: s) n)
⊢ a = b ∨ a ∈ s
[PROOFSTEP]
cases' n with n'
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = nth (b :: s) zero
⊢ a = b ∨ a ∈ s
[PROOFSTEP]
left
[GOAL]
case zero.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = nth (b :: s) zero
⊢ a = b
[PROOFSTEP]
exact h
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth (b :: s) (succ n')
⊢ a = b ∨ a ∈ s
[PROOFSTEP]
right
[GOAL]
case succ.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth (b :: s) (succ n')
⊢ a ∈ s
[PROOFSTEP]
rw [nth_succ, tail_cons] at h
[GOAL]
case succ.h
α : Type u
β : Type v
δ : Type w
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = nth s n'
⊢ a ∈ s
[PROOFSTEP]
exact ⟨n', h⟩
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
s : Stream' α
⊢ map f s = f (head s) :: map f (tail s)
[PROOFSTEP]
rw [← Stream'.eta (map f s), tail_map, head_map]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
s : Stream' α
⊢ map f (a :: s) = f a :: map f s
[PROOFSTEP]
rw [← Stream'.eta (map f (a :: s)), map_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
s : Stream' α
⊢ head (f (head (a :: s)) :: map f (tail (a :: s))) :: tail (f (head (a :: s)) :: map f (tail (a :: s))) =
    f a :: map f s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b => a = b) (nth s n)
⊢ (fun b => f a = b) (nth (map f s) n)
[PROOFSTEP]
rw [nth_map, h]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ zip f s₁ s₂ = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂)
[PROOFSTEP]
rw [← Stream'.eta (zip f s₁ s₂)]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ head (zip f s₁ s₂) :: tail (zip f s₁ s₂) = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
⊢ const a = a :: const a
[PROOFSTEP]
apply Stream'.ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
a : α
⊢ ∀ (n : ℕ), nth (const a) n = nth (a :: const a) n
[PROOFSTEP]
intro n
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
a : α
n : ℕ
⊢ nth (const a) n = nth (a :: const a) n
[PROOFSTEP]
cases n
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
a : α
⊢ nth (const a) zero = nth (a :: const a) zero
[PROOFSTEP]
rfl
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
a : α
n✝ : ℕ
⊢ nth (const a) (succ n✝) = nth (a :: const a) (succ n✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
this : tail (a :: const a) = const a
⊢ tail (const a) = const a
[PROOFSTEP]
rwa [← const_eq] at this
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ tail (iterate f a) = iterate f (f a)
[PROOFSTEP]
ext n
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ nth (tail (iterate f a)) n = nth (iterate f (f a)) n
[PROOFSTEP]
rw [nth_tail]
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ nth (iterate f a) (n + 1) = nth (iterate f (f a)) n
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ nth (iterate f a) (zero + 1) = nth (iterate f (f a)) zero
[PROOFSTEP]
rfl
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n' : ℕ
ih : nth (iterate f a) (n' + 1) = nth (iterate f (f a)) n'
⊢ nth (iterate f a) (succ n' + 1) = nth (iterate f (f a)) (succ n')
[PROOFSTEP]
rw [nth_succ_iterate', ih, nth_succ_iterate']
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)
[PROOFSTEP]
rw [← Stream'.eta (iterate f a)]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ head (iterate f a) :: tail (iterate f a) = a :: iterate f (f a)
[PROOFSTEP]
rw [tail_iterate]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ head (iterate f a) :: iterate f (f a) = a :: iterate f (f a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
f : α → α
a : α
⊢ nth (iterate f a) (succ n) = nth (iterate f (f a)) n
[PROOFSTEP]
rw [nth_succ, tail_iterate]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ head s₁ = head s₂ ∧ (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) (tail s₁) (tail s₂)
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ head s₁ = head s₂
case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) (tail s₁) (tail s₂)
[PROOFSTEP]
exact h₁
[GOAL]
case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) (tail s₁) (tail s₂)
[PROOFSTEP]
rw [← h₂, ← h₃]
[GOAL]
case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
[PROOFSTEP]
repeat' constructor
[GOAL]
case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
[PROOFSTEP]
constructor
[GOAL]
case right.left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ head s₁ = head s₂
[PROOFSTEP]
constructor
[GOAL]
case right.right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ s₁ = tail s₁ ∧ s₂ = tail s₂
[PROOFSTEP]
constructor
[GOAL]
case right.right.left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ s₁ = tail s₁
[PROOFSTEP]
constructor
[GOAL]
case right.right.right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ s₂ = tail s₂
[PROOFSTEP]
constructor
[GOAL]
case right.left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ head s₁ = head s₂
[PROOFSTEP]
assumption
[GOAL]
case right.right.left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ s₁ = tail s₁
[PROOFSTEP]
assumption
[GOAL]
case right.right.right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ : Stream' α
hh : head s₁✝ = head s₂✝
ht₁ : s₁✝ = tail s₁✝
ht₂ : s₂✝ = tail s₂✝
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ => head s₁ = head s₂ ∧ s₁ = tail s₁ ∧ s₂ = tail s₂) s₁ s₂
h₁ : head s₁ = head s₂
h₂ : s₁ = tail s₁
h₃ : s₂ = tail s₂
⊢ s₂ = tail s₂
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β✝ : Type v
δ : Type w
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (tail (iterate id a)) = fr (tail (const a))
[PROOFSTEP]
rw [tail_iterate, tail_const]
[GOAL]
α : Type u
β✝ : Type v
δ : Type w
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id (id a)) = fr (const a)
[PROOFSTEP]
exact ch
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ iterate f (f a) = map f (iterate f a)
[PROOFSTEP]
funext n
[GOAL]
case h
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ iterate f (f a) n = map f (iterate f a) n
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case h.zero
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ iterate f (f a) zero = map f (iterate f a) zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = map f (iterate f a) n'
⊢ iterate f (f a) (succ n') = map f (iterate f a) (succ n')
[PROOFSTEP]
unfold map iterate nth
[GOAL]
case h.succ
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = map f (iterate f a) n'
⊢ f (iterate f (f a) n') = f (iterate f a (succ n'))
[PROOFSTEP]
rw [map, nth] at ih
[GOAL]
case h.succ
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = f (iterate f a n')
⊢ f (iterate f (f a) n') = f (iterate f a (succ n'))
[PROOFSTEP]
rw [iterate]
[GOAL]
case h.succ
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = f (iterate f a n')
⊢ f (iterate f (f a) n') = f (f (iterate f a n'))
[PROOFSTEP]
exact congrArg f ih
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
g : α → α
a : α
⊢ corec f g a = f a :: corec f g (g a)
[PROOFSTEP]
rw [corec_def, map_eq, head_iterate, tail_iterate]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
⊢ corec id id a = const a
[PROOFSTEP]
rw [corec_def, map_id, iterate_id]
[GOAL]
α : Type u
β : Type v
δ : Type w
g : α → β
f : α → α
a : α
⊢ unfolds g f a = g a :: unfolds g f (f a)
[PROOFSTEP]
unfold unfolds
[GOAL]
α : Type u
β : Type v
δ : Type w
g : α → β
f : α → α
a : α
⊢ corec g f a = g a :: corec g f (f a)
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), nth (unfolds head tail s) n = nth s n
[PROOFSTEP]
intro n
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) n = nth s n
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) zero = nth s zero
[PROOFSTEP]
intro s
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ nth (unfolds head tail s) zero = nth s zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (unfolds head tail s) n' = nth s n'
⊢ ∀ (s : Stream' α), nth (unfolds head tail s) (succ n') = nth s (succ n')
[PROOFSTEP]
intro s
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (unfolds head tail s) n' = nth s n'
s : Stream' α
⊢ nth (unfolds head tail s) (succ n') = nth s (succ n')
[PROOFSTEP]
rw [nth_succ, nth_succ, unfolds_eq, tail_cons, ih]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
[PROOFSTEP]
let t := tail s₁ ⋈ tail s₂
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
[PROOFSTEP]
show s₁ ⋈ s₂ = head s₁ :: head s₂ :: t
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: t
[PROOFSTEP]
unfold interleave
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ (corecOn (s₁, s₂)
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      fun x =>
      match x with
      | (s₁, s₂) => (s₂, tail s₁)) =
    head s₁ :: head s₂ :: t
[PROOFSTEP]
unfold corecOn
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₁, s₂) =
    head s₁ :: head s₂ :: t
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ (match (s₁, s₂) with
      | (s₁, snd) => head s₁) ::
      corec
        (fun x =>
          match x with
          | (s₁, snd) => head s₁)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, tail s₁))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, tail s₁)) =
    head s₁ :: head s₂ :: t
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ head s₁ :: corec (fun x => head x.fst) (fun x => (x.snd, tail x.fst)) (s₂, tail s₁) =
    head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ head s₁ ::
      head (s₂, tail s₁).fst ::
        corec (fun x => head x.fst) (fun x => (x.snd, tail x.fst)) ((s₂, tail s₁).snd, tail (s₂, tail s₁).fst) =
    head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail (s₁ ⋈ s₂) = s₂ ⋈ tail s₁
[PROOFSTEP]
unfold interleave corecOn
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail
      (corec
        (fun x =>
          match x with
          | (s₁, snd) => head s₁)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, tail s₁))
        (s₁, s₂)) =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₂, tail s₁)
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail
      ((match (s₁, s₂) with
        | (s₁, snd) => head s₁) ::
        corec
          (fun x =>
            match x with
            | (s₁, snd) => head s₁)
          (fun x =>
            match x with
            | (s₁, s₂) => (s₂, tail s₁))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, tail s₁))) =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₂, tail s₁)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail s₁ ⋈ tail s₂ = tail (tail (s₁ ⋈ s₂))
[PROOFSTEP]
rw [interleave_eq s₁ s₂]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail s₁ ⋈ tail s₂ = tail (tail (head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (2 * (n + 1)) = nth s₁ (n + 1)
[PROOFSTEP]
change nth (s₁ ⋈ s₂) (succ (succ (2 * n))) = nth s₁ (succ n)
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (succ (succ (2 * n))) = nth s₁ (succ n)
[PROOFSTEP]
rw [nth_succ, nth_succ, interleave_eq, tail_cons, tail_cons]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (tail s₁ ⋈ tail s₂) (2 * n) = nth s₁ (succ n)
[PROOFSTEP]
have : n < succ n := Nat.lt_succ_self n
[GOAL]
α : 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)
[PROOFSTEP]
rw [nth_interleave_left n (tail s₁) (tail s₂)]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
this : n < succ n
⊢ nth (tail s₁) n = nth s₁ (succ n)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (2 * (n + 1) + 1) = nth s₂ (n + 1)
[PROOFSTEP]
change nth (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = nth s₂ (succ n)
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = nth s₂ (succ n)
[PROOFSTEP]
rw [nth_succ, nth_succ, interleave_eq, tail_cons, tail_cons, nth_interleave_right n (tail s₁) (tail s₂)]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s₁ s₂ : Stream' α
⊢ nth (tail s₂) n = nth s₂ (succ n)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₁
n : ℕ
h : (fun b => a = b) (nth s₁ n)
⊢ (fun b => a = b) (nth (s₁ ⋈ s₂) (2 * n))
[PROOFSTEP]
rw [h, nth_interleave_left]
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₂
n : ℕ
h : (fun b => a = b) (nth s₂ n)
⊢ (fun b => a = b) (nth (s₁ ⋈ s₂) (2 * n + 1))
[PROOFSTEP]
rw [h, nth_interleave_right]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (even s) = even (tail (tail s))
[PROOFSTEP]
unfold even
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (corec (fun s => head s) (fun s => tail (tail s)) s) =
    corec (fun s => head s) (fun s => tail (tail s)) (tail (tail s))
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (head s :: corec (fun s => head s) (fun s => tail (tail s)) (tail (tail s))) =
    corec (fun s => head s) (fun s => tail (tail s)) (tail (tail s))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a₁ a₂ : α
s : Stream' α
⊢ even (a₁ :: a₂ :: s) = a₁ :: even s
[PROOFSTEP]
unfold even
[GOAL]
α : Type u
β : Type v
δ : Type w
a₁ a₂ : α
s : Stream' α
⊢ corec (fun s => head s) (fun s => tail (tail s)) (a₁ :: a₂ :: s) =
    a₁ :: corec (fun s => head s) (fun s => tail (tail s)) s
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
a₁ a₂ : α
s : Stream' α
⊢ head (a₁ :: a₂ :: s) :: corec (fun s => head s) (fun s => tail (tail s)) (tail (tail (a₁ :: a₂ :: s))) =
    a₁ :: corec (fun s => head s) (fun s => tail (tail s)) s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head s₁' = head s₁ ∧ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail s₁') (tail s₁)
[PROOFSTEP]
rw [h₁]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head (even (s₁ ⋈ s₂)) = head s₁ ∧ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail (even (s₁ ⋈ s₂))) (tail s₁)
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head (even (s₁ ⋈ s₂)) = head s₁
[PROOFSTEP]
rfl
[GOAL]
case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail (even (s₁ ⋈ s₂))) (tail s₁)
[PROOFSTEP]
exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ tail (even (s₁ ⋈ s₂)) = even (tail s₁ ⋈ tail s₂)
[PROOFSTEP]
rw [interleave_eq, even_cons_cons, tail_cons]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s' s : Stream' α
h : s' = even s ⋈ odd s
⊢ head s' = head s ∧ (fun s' s => s' = even s ⋈ odd s) (tail s') (tail s)
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s' s : Stream' α
h : s' = even s ⋈ odd s
⊢ head (even s ⋈ odd s) = head s ∧ (fun s' s => s' = even s ⋈ odd s) (tail (even s ⋈ odd s)) (tail s)
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
δ : Type w
s₁ s' s : Stream' α
h : s' = even s ⋈ odd s
⊢ head (even s ⋈ odd s) = head s
[PROOFSTEP]
rfl
[GOAL]
case right
α : Type u
β : Type v
δ : Type w
s₁ s' s : Stream' α
h : s' = even s ⋈ odd s
⊢ (fun s' s => s' = even s ⋈ odd s) (tail (even s ⋈ odd s)) (tail s)
[PROOFSTEP]
simp [odd_eq, odd_eq, tail_interleave, tail_even]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (even s) (succ n) = nth s (2 * succ n)
[PROOFSTEP]
change nth (even s) (succ n) = nth s (succ (succ (2 * n)))
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (even s) (succ n) = nth s (succ (succ (2 * n)))
[PROOFSTEP]
rw [nth_succ, nth_succ, tail_even, nth_even n]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (tail (tail s)) (2 * n) = nth (tail s) (2 * n + 1)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (odd s) n = nth s (2 * n + 1)
[PROOFSTEP]
rw [odd_eq, nth_even]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ nth (tail s) (2 * n) = nth s (2 * n + 1)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
s : Stream' α
x✝ : a ∈ even s
n : ℕ
h : (fun b => a = b) (nth (even s) n)
⊢ (fun b => a = b) (nth s (2 * n))
[PROOFSTEP]
rw [h, nth_even]
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
s : Stream' α
x✝ : a ∈ odd s
n : ℕ
h : (fun b => a = b) (nth (odd s) n)
⊢ (fun b => a = b) (nth s (2 * n + 1))
[PROOFSTEP]
rw [h, nth_odd]
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)
[PROOFSTEP]
rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]
[GOAL]
α : Type u
β : Type v
δ : Type w
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s
[PROOFSTEP]
rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ drop (List.length []) ([] ++ₛ s) = s
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
l : List α
s : Stream' α
⊢ drop (List.length (a :: l)) (a :: l ++ₛ s) = s
[PROOFSTEP]
rw [List.length_cons, drop_succ, cons_append_stream, tail_cons, drop_append_stream l s]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ [head s] ++ₛ tail s = s
[PROOFSTEP]
rw [cons_append_stream, nil_append_stream, Stream'.eta]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [nth s (n + 1)]
[PROOFSTEP]
rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, nth_tail]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
s : Stream' α
⊢ List.length (take n s) = n
[PROOFSTEP]
induction n generalizing s
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ List.length (take zero s) = zero
[PROOFSTEP]
simp [*, take_succ]
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
n_ih✝ : ∀ (s : Stream' α), List.length (take n✝ s) = n✝
s : Stream' α
⊢ List.length (take (succ n✝) s) = succ n✝
[PROOFSTEP]
simp [*, take_succ]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s
[PROOFSTEP]
rw [min_zero, List.take_zero, take_zero]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s
[PROOFSTEP]
rw [zero_min, take_zero, List.take_nil]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
m n : ℕ
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
[PROOFSTEP]
rw [take_succ, List.take_cons, Nat.min_succ_succ, take_succ, take_take]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ List.get? (take (n + 1) s) (k + 1) = some (nth s (k + 1))
[PROOFSTEP]
rw [take_succ, List.get?, get?_take (Nat.lt_of_succ_lt_succ h), nth_succ]
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
xs : Stream' α
⊢ List.dropLast (take n xs) = take (n - 1) xs
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
xs : Stream' α
⊢ List.dropLast (take zero xs) = take (zero - 1) xs
case succ
α : Type u
β : Type v
δ : Type w
xs : Stream' α
n✝ : ℕ
⊢ List.dropLast (take (succ n✝) xs) = take (succ n✝ - 1) xs
[PROOFSTEP]
case zero => simp
[GOAL]
α : Type u
β : Type v
δ : Type w
xs : Stream' α
⊢ List.dropLast (take zero xs) = take (zero - 1) xs
[PROOFSTEP]
case zero => simp
[GOAL]
α : Type u
β : Type v
δ : Type w
xs : Stream' α
⊢ List.dropLast (take zero xs) = take (zero - 1) xs
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
xs : Stream' α
n✝ : ℕ
⊢ List.dropLast (take (succ n✝) xs) = take (succ n✝ - 1) xs
[PROOFSTEP]
case succ n => rw [take_succ', List.dropLast_concat, Nat.succ_sub_one]
[GOAL]
α : Type u
β : Type v
δ : Type w
xs : Stream' α
n : ℕ
⊢ List.dropLast (take (succ n) xs) = take (succ n - 1) xs
[PROOFSTEP]
case succ n => rw [take_succ', List.dropLast_concat, Nat.succ_sub_one]
[GOAL]
α : Type u
β : Type v
δ : Type w
xs : Stream' α
n : ℕ
⊢ List.dropLast (take (succ n) xs) = take (succ n - 1) xs
[PROOFSTEP]
rw [take_succ', List.dropLast_concat, Nat.succ_sub_one]
[GOAL]
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), take n s ++ₛ drop n s = s
[PROOFSTEP]
intro n
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), take n s ++ₛ drop n s = s
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), take zero s ++ₛ drop zero s = s
[PROOFSTEP]
intro s
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ take zero s ++ₛ drop zero s = s
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
⊢ ∀ (s : Stream' α), take (succ n') s ++ₛ drop (succ n') s = s
[PROOFSTEP]
intro s
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
s : Stream' α
⊢ take (succ n') s ++ₛ drop (succ n') s = s
[PROOFSTEP]
rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ (∀ (n : ℕ), take n s₁ = take n s₂) → s₁ = s₂
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂
[PROOFSTEP]
apply Stream'.ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ ∀ (n : ℕ), nth s₁ n = nth s₂ n
[PROOFSTEP]
intro n
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ nth s₁ n = nth s₂ n
[PROOFSTEP]
induction' n with n _
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ nth s₁ zero = nth s₂ zero
[PROOFSTEP]
have aux := h 1
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : take 1 s₁ = take 1 s₂
⊢ nth s₁ zero = nth s₂ zero
[PROOFSTEP]
simp [take] at aux
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
aux : head s₁ = head s₂
⊢ nth s₁ zero = nth s₂ zero
[PROOFSTEP]
exact aux
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
⊢ nth s₁ (succ n) = nth s₂ (succ n)
[PROOFSTEP]
have h₁ : some (nth s₁ (succ n)) = some (nth s₂ (succ n)) := by
  rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]
[GOAL]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
⊢ some (nth s₁ (succ n)) = some (nth s₂ (succ n))
[PROOFSTEP]
rw [← get?_take_succ, ← get?_take_succ, h (succ (succ n))]
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
n_ih✝ : nth s₁ n = nth s₂ n
h₁ : some (nth s₁ (succ n)) = some (nth s₂ (succ n))
⊢ nth s₁ (succ n) = nth s₂ (succ n)
[PROOFSTEP]
injection h₁
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
⊢ ∀ (l' : List α) (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
intro l'
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
l' : List α
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
induction' l' with a₁ l₁ ih
[GOAL]
case nil
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', [], a, l) = [a'] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
intros
[GOAL]
case nil
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
a'✝ : α
⊢ corec Stream'.cycleF Stream'.cycleG (a'✝, [], a, l) = [a'✝] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
rw [corec_eq]
[GOAL]
case nil
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
a'✝ : α
⊢ Stream'.cycleF (a'✝, [], a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a'✝, [], a, l)) =
    [a'✝] ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
⊢ ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
      a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
intros
[GOAL]
case cons
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a'✝ : α
⊢ corec Stream'.cycleF Stream'.cycleG (a'✝, a₁ :: l₁, a, l) =
    a'✝ :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
rw [corec_eq, Stream'.cycle_g_cons, ih a₁]
[GOAL]
case cons
α : Type u
β : Type v
δ : Type w
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a'✝ : α
⊢ Stream'.cycleF (a'✝, a₁ :: l₁, a, l) :: (a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)) =
    a'✝ :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ cycle l h
[PROOFSTEP]
rw [cycle_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ l ++ₛ cycle l h
[PROOFSTEP]
exact mem_append_stream_left _ ainl
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
⊢ [a] ≠ []
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : Type v
δ : Type w
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] (_ : ¬[a] = [])) = fr (const a)
⊢ fr (tail (cycle [a] (_ : ¬[a] = []))) = fr (tail (const a))
[PROOFSTEP]
rwa [cycle_eq, const_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tails s = tail s :: tails (tail s)
[PROOFSTEP]
unfold tails
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ corec id tail (tail s) = tail s :: corec id tail (tail (tail s))
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ id (tail s) :: corec id tail (tail (tail s)) = tail s :: corec id tail (tail (tail s))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), nth (tails s) n = drop n (tail s)
[PROOFSTEP]
intro n
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (tails s) n = drop n (tail s)
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (tails s) zero = drop zero (tail s)
[PROOFSTEP]
intros
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
s✝ : Stream' α
⊢ nth (tails s✝) zero = drop zero (tail s✝)
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (tails s) n' = drop n' (tail s)
⊢ ∀ (s : Stream' α), nth (tails s) (succ n') = drop (succ n') (tail s)
[PROOFSTEP]
intro s
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (tails s) n' = drop n' (tail s)
s : Stream' α
⊢ nth (tails s) (succ n') = drop (succ n') (tail s)
[PROOFSTEP]
rw [nth_succ, drop_succ, tails_eq, tail_cons, ih]
[GOAL]
α : Type u
β : Type v
δ : Type w
l : List α
s : Stream' α
⊢ initsCore l s = l :: initsCore (l ++ [head s]) (tail s)
[PROOFSTEP]
unfold initsCore corecOn
[GOAL]
α : Type u
β : Type v
δ : Type w
l : List α
s : Stream' α
⊢ corec
      (fun x =>
        match x with
        | (a, snd) => a)
      (fun p =>
        match p with
        | (l', s') => (l' ++ [head s'], tail s'))
      (l, s) =
    l ::
      corec
        (fun x =>
          match x with
          | (a, snd) => a)
        (fun p =>
          match p with
          | (l', s') => (l' ++ [head s'], tail s'))
        (l ++ [head s], tail s)
[PROOFSTEP]
rw [corec_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (inits s) = initsCore [head s, head (tail s)] (tail (tail s))
[PROOFSTEP]
unfold inits
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail (initsCore [head s] (tail s)) = initsCore [head s, head (tail s)] (tail (tail s))
[PROOFSTEP]
rw [inits_core_eq]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ tail ([head s] :: initsCore ([head s] ++ [head (tail s)]) (tail (tail s))) =
    initsCore [head s, head (tail s)] (tail (tail s))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
⊢ ∀ (a : α) (n : ℕ) (l : List α) (s : Stream' α), a :: nth (initsCore l s) n = nth (initsCore (a :: l) s) n
[PROOFSTEP]
intro a n
[GOAL]
α : Type u
β : Type v
δ : Type w
a : α
n : ℕ
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n = nth (initsCore (a :: l) s) n
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
a : α
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) zero = nth (initsCore (a :: l) s) zero
[PROOFSTEP]
intros
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
a : α
l✝ : List α
s✝ : Stream' α
⊢ a :: nth (initsCore l✝ s✝) zero = nth (initsCore (a :: l✝) s✝) zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
⊢ ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) (succ n') = nth (initsCore (a :: l) s) (succ n')
[PROOFSTEP]
intro l s
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
l : List α
s : Stream' α
⊢ a :: nth (initsCore l s) (succ n') = nth (initsCore (a :: l) s) (succ n')
[PROOFSTEP]
rw [nth_succ, inits_core_eq, tail_cons, ih, inits_core_eq (a :: l) s]
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
a : α
n' : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: nth (initsCore l s) n' = nth (initsCore (a :: l) s) n'
l : List α
s : Stream' α
⊢ nth (initsCore (a :: (l ++ [head s])) (tail s)) n' =
    nth ((a :: l) :: initsCore (a :: l ++ [head s]) (tail s)) (succ n')
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ) (s : Stream' α), nth (inits s) n = take (succ n) s
[PROOFSTEP]
intro n
[GOAL]
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ ∀ (s : Stream' α), nth (inits s) n = take (succ n) s
[PROOFSTEP]
induction' n with n' ih
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
⊢ ∀ (s : Stream' α), nth (inits s) zero = take (succ zero) s
[PROOFSTEP]
intros
[GOAL]
case zero
α : Type u
β : Type v
δ : Type w
s✝ : Stream' α
⊢ nth (inits s✝) zero = take (succ zero) s✝
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (inits s) n' = take (succ n') s
⊢ ∀ (s : Stream' α), nth (inits s) (succ n') = take (succ (succ n')) s
[PROOFSTEP]
intros
[GOAL]
case succ
α : Type u
β : Type v
δ : Type w
n' : ℕ
ih : ∀ (s : Stream' α), nth (inits s) n' = take (succ n') s
s✝ : Stream' α
⊢ nth (inits s✝) (succ n') = take (succ (succ n')) s✝
[PROOFSTEP]
rw [nth_succ, take_succ, ← ih, tail_inits, inits_tail, cons_nth_inits_core]
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ inits s = [head s] :: map (List.cons (head s)) (inits (tail s))
[PROOFSTEP]
apply Stream'.ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ ∀ (n : ℕ), nth (inits s) n = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) n
[PROOFSTEP]
intro n
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ nth (inits s) n = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) n
[PROOFSTEP]
cases n
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ nth (inits s) zero = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) zero
[PROOFSTEP]
rfl
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ nth (inits s) (succ n✝) = nth ([head s] :: map (List.cons (head s)) (inits (tail s))) (succ n✝)
[PROOFSTEP]
rw [nth_inits, nth_succ, tail_cons, nth_map, nth_inits]
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
s : Stream' α
n✝ : ℕ
⊢ take (succ (succ n✝)) s = head s :: take (succ n✝) (tail s)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ zip appendStream' (inits s) (tails s) = const s
[PROOFSTEP]
apply Stream'.ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
⊢ ∀ (n : ℕ), nth (zip appendStream' (inits s) (tails s)) n = nth (const s) n
[PROOFSTEP]
intro n
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ nth (zip appendStream' (inits s) (tails s)) n = nth (const s) n
[PROOFSTEP]
rw [nth_zip, nth_inits, nth_tails, nth_const, take_succ, cons_append_stream, append_take_drop, Stream'.eta]
[GOAL]
α : Type u
β : Type v
δ : Type w
⊢ nats = 0 :: map succ nats
[PROOFSTEP]
apply Stream'.ext
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
⊢ ∀ (n : ℕ), nth nats n = nth (0 :: map succ nats) n
[PROOFSTEP]
intro n
[GOAL]
case a
α : Type u
β : Type v
δ : Type w
n : ℕ
⊢ nth nats n = nth (0 :: map succ nats) n
[PROOFSTEP]
cases n
[GOAL]
case a.zero
α : Type u
β : Type v
δ : Type w
⊢ nth nats zero = nth (0 :: map succ nats) zero
case a.succ α : Type u β : Type v δ : Type w n✝ : ℕ ⊢ nth nats (succ n✝) = nth (0 :: map succ nats) (succ n✝)
[PROOFSTEP]
rfl
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth nats (succ n✝) = nth (0 :: map succ nats) (succ n✝)
[PROOFSTEP]
rw [nth_succ]
[GOAL]
case a.succ
α : Type u
β : Type v
δ : Type w
n✝ : ℕ
⊢ nth (tail nats) n✝ = nth (0 :: map succ nats) (succ n✝)
[PROOFSTEP]
rfl