case a
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ nth (tail (iterate f a)) n = nth (iterate f (f a)) n
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ tail (iterate f a) = iterate f (f a)
ext n
case a
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ nth (iterate f a) (n + 1) = nth (iterate f (f a)) n
case a
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ nth (tail (iterate f a)) n = nth (iterate f (f a)) n
rw [nth_tail]
case a.zero
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ nth (iterate f a) (zero + 1) = nth (iterate f (f a)) zero

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')
case a
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ nth (iterate f a) (n + 1) = nth (iterate f (f a)) n
induction' n with n' ih
no goals
case a.zero
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ nth (iterate f a) (zero + 1) = nth (iterate f (f a)) zero
rfl
no goals
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')
rw [nth_succ_iterate', ih, nth_succ_iterate']