Pigeonhole into ∏_{q | n} Fin q avoids CRT in Thue/Legendre-type proofs

For lattice or pigeonhole arguments needing a congruence mod a squarefree n, such as Legendre's ax^2+by^2=cz^2, don't build a residue mod n via CRT. Get one linear form L_q per prime with choose! α β γ hL using ... over q ∈ n.primeFactors. Then map the box into the dependent product ((q : n.primeFactors) → Fin q) by ⟨((L q ...) % q).toNat, _⟩. Its Fintype.card is ∏ q = n by Fintype.card_pi, Finset.prod_coe_sort and Nat.prod_primeFactors_of_squarefree. Fintype.exists_ne_map_eq_of_card_lt gives the collision. Recover n ∣ Q with Finset.prod_dvd_of_coprime, using Nat.isCoprime_iff_coprime and Nat.coprime_primes for the pairwise condition. Box sizes come from Nat.sqrt with Nat.lt_succ_sqrt' and Nat.sqrt_le', so no reals are needed. Gotcha: when passing a 'by' proof to a lemma with an implicit k, give (k := k) explicitly, or ring_nf may assign the metavariable to something wrong.