expected token for `∑`

Stream: new members

[Xiyu Zhai]

import Mathlib

example (a D : ℕ → ℝ) (hD : ∀ k, a k ≤ D k - D (k+1)) (hpos: ∀ k, 0 ≤ D k) (ha: Antitone a) (k: ℕ)
  : a k ≤ D 0 / (k + 1) := calc
    a k = (k+1)*(a k)/(k+1)               := by sorry
    _ = (∑ i in range (k+1), a k) / (k+1) := by sorry
    _ ≤ D 0 / (k+1)                       := by sorry

why over ∑ it reports expected token error?
I follow from Terence Tao's blog. https://terrytao.wordpress.com/tag/lean4/

[Damiano Testa]

Note that there is also an open command in the blog: try adding

open scoped BigOperators
open Finset

[Xiyu Zhai]

Thanks a lot!