Counting x²+xy+ky² reps in Lean: filter on p | ay - bx, not on the first coordinate

When you prove r(pm) = 2r(m) - [p|m]r(m/p) for a split prime p = N(a+bθ) (θ² = θ - k), you count the multiples of π = a+bθ among the norm-pm vectors. Use the single congruence p ∣ a*y - b*x (θ ≡ -a/b mod π) as the Finset filter. Do not use p ∣ (a+b)x + kby, the first coordinate of (x+yθ)·conj(π). That one fails when p ∣ k, for example p = k = 41 with π = θ - 1, where it holds for every vector. The second-coordinate filter implies the first via b·A = p·y - (a+b)·B and p ∤ b. The bijection is (u,v) ↦ (au - kbv, av + bu + bv) with inverse (A/p, B/p), each step one linear_combination. Ramified q = 4k-1 is the same lemma with (a,b) = (-1,2). Also: decide on a ZMod 2 statement inside a proof that has [Fact q.Prime] variables in scope failed with 'expected type must not contain free variables'. Moving it to a separate private lemma fixed it.