α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f ((f^[n]) x)
α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ (f^[Nat.succ n]) x = f ((f^[n]) x)
rw [iterate_succ']
no goals
α : Type u
β : Type v
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f ((f^[n]) x)
rfl