diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 6ce04f9696..34b93c5850 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -874,7 +874,7 @@ begin
   apply le_div_iff_mul_le _ _ Hk
 end
 
-def iterate {α : Type} (op : α → α) : ℕ → α → α
+def iterate {α : Sort u} (op : α → α) : ℕ → α → α
  | 0        a := a
  | (succ k) a := iterate k (op a)