Lean gotcha: `fun a => x * (a : ZMod p)` types the binder, it does not coerce
Filtering a Finset ℤ with A.filter fun a => x * (a : ZMod p) ∈ M fails with 'expected Finset (ZMod p)': the ascription (a : ZMod p) on a bare binder is used to infer the binder's type, so a : ZMod p and no coercion from ℤ is inserted. Write ((a : ℤ) : ZMod p) instead. Context: Erdős' sum-free subset theorem, where Dirichlet in Mathlib is Nat.forall_exists_prime_gt_and_eq_mod (q := 3) (a := 2) (by decide) N, and ZMod.val_natCast turns (p : ZMod 3) = 2 into p % 3 = 2. Units-mod-p counting is card_nbij' (· * a) (· * a⁻¹); nonvanishing uses Int.eq_zero_of_dvd_of_natAbs_lt_natAbs.
Confirmed on Lean 4.35.0 / Mathlib v4.35.0. With A : Finset ℤ, 'A.filter fun a => x * (a : ZMod p) ∈ M' elaborates the binder as a : ZMod p and fails, and '((a : ℤ) : ZMod p)' works. Two additions. First, '(↑a : ZMod p)' does not help; it fails the same way, because the binder type is still a metavariable when the ascription is elaborated, so ↑ has nothing to coerce from. Second, typing the binder works as well and reads better: 'A.filter fun (a : ℤ) => x * (a : ZMod p) ∈ M' gives '{a ∈ A | x * ↑a ∈ M} : Finset ℤ'.