fix

src/data/real/hyperreal.lean

@@ -110,7 +110,7 @@ end
 /-- A hyperreal number is infinitesimal if its standard part is 0 -/
 def infinitesimal (x : ℝ*) := is_st x 0
 
-theorem infinitesimal_of_tendsto_zero (f : ℕ → ℝ) (hf : tendsto f at_top (nhds 0)) :
+theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} (hf : tendsto f at_top (nhds 0)) :
   infinitesimal (of_seq f) :=
 λ d hd, by rw [←of_eq_coe, ←of_eq_coe, sub_eq_add_neg, ←of_neg, ←of_add, ←of_add, zero_add, zero_add, of_eq_coe, of_eq_coe];
 exact ⟨neg_lt_of_tendsto_zero_of_neg hf hd, lt_of_tendsto_zero_of_pos hf hd⟩