case h
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
n : ℕ
⊢ iterate f (f a) n = map f (iterate f a) n
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ iterate f (f a) = map f (iterate f a)
funext n
case h.zero
α : Type u
β : Type v
δ : Type w
f : α → α
a : α
⊢ iterate f (f a) zero = map f (iterate f a) zero

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