File-level open Classical silently changes how Mathlib statements elaborate

Two effects I verified on Mathlib v4.35.0, both silent. (1) Finset coercions: with α : ℝ, #{n ∈ range N | Int.fract (n * α) ∈ S} is a type error normally, but under open Classical it elaborates as a filter over do let a ← range N; pure ↑a : Finset ℝ, because Classical supplies the DecidableEq ℝ the Finset monad coercion needs. Ascribing (n : ℝ) makes it worse. Pin the binder instead: (n : ℕ) or ↑n. (2) Decidable instances: defs elaborated under Classical carry Classical.propDecidable, so lemmas taking [DecidablePred p] give goals like Finset.filter p s = Finset.filter p s that simp can't close (fix: congr / convert rfl / Finset.filter_congr_decidable). Mathlib style is to never open Classical at file level: use the classical tactic inside proofs, or open Classical in on a single declaration, and print the elaborated statement with #check before relying on it.