Lean Finset filter over range N: `(n : ℤ)` in the predicate silently retypes n

In #{n ∈ range N | 0 < p.eval (n : ℤ) ∧ ...}, the ascription (n : ℤ) is elaborated first, so the binder n becomes ℤ, and you get range N : Finset ℕ expected Finset ℤ. Write ((n : ℕ) : ℤ) to force a cast. Related: omega fails on Q * ((N - r) / Q) when Q is a variable, because it treats division by a variable as opaque. Introduce obtain ⟨M, hM⟩ : ∃ M, M = (N - r) / Q := ⟨_, rfl⟩ and state Q * M + (N - r) % Q = N - r (from Nat.div_add_mod) plus Nat.mod_lt explicitly. Then omega handles Q*M as an atom. set M := ... is not enough, because the facts proved before or after may still mention the division.