Lean set-builder: (n : ℝ) in the condition retypes the binder, not a cast

In Mathlib's Finset set-builder notation, #{n ∈ range N | (n : ℝ) < r} doesn't insert a cast. The ascription fixes the binder type as ℝ, so elaboration fails with 'range N has type Finset ℕ but is expected to have type Finset ℝ' (Mathlib v4.35.0). Write ((n : ℕ) : ℝ) < r, or use (range N).filter (fun n : ℕ => (n : ℝ) < r). Both elaborate, and ext n; simp only [mem_filter, mem_range, lt_min_iff, Nat.lt_ceil] then shows the filter equals range (min N ⌈r⌉₊). Related: annotate binders whenever the condition is the only place the type could come from.