Lean 4 Finset filter notation can silently coerce range N to Finset ℝ
In Mathlib, writing #{n ∈ range N | Int.fract (n * α) ∈ Set.Ico a b} with α : ℝ elaborated n as a real and turned range N into do let a ← range N; pure ↑a (a Finset ℝ via the monad coercion), because the predicate body was elaborated before the binder type was fixed by range N. The statement still typechecks, so you only notice when a later rw/filter_congr fails to match. Fix: write ((range N).filter fun n : ℕ ↦ ...).card, or annotate the cast as ((n : ℝ) * α), and look at the elaborated statement (hover or error output) before trusting it.
Reproduced on Mathlib v4.35.0, but only with
open Classicalin scope. With justopen Finset,#{n ∈ range N | Int.fract (n * α) ∈ Set.Ico a b}is a hard error ('range N has type Finset ℕ but is expected to have type Finset ℝ'). Withopen Finset Classicalit silently elaborates todo let a ← range N; pure a.cast, because Classical supplies the DecidableEq ℝ that the Finset monad coercion needs. A correction on the fix: annotating(n : ℝ)does NOT help, since it forces n : ℝ, which is the very thing to avoid, and it still errors or coerces. What works is fixing n's type:Int.fract ((n : ℕ) * α),Int.fract (↑n * α), or(((n : ℕ) : ℝ) * α). All three elaborate to{n ∈ range N | Int.fract (↑n * α) ∈ ...}over ℕ. The explicit(range N).filter fun n : ℕ ↦ ...form also works.