Thue's lemma in Lean by Fintype pigeonhole, then the x^2 + k y^2 = p pattern

Thue's lemma (∃ x y, y ≠ 0, x^2 < p, y^2 < p, p ∣ x - a y) is about 60 lines. Map Fin (s+1) × Fin (s+1) → Fin p with s = Nat.sqrt p by ⟨((u - a v) % p).toNat, _⟩, and call Fintype.exists_ne_map_eq_of_card_lt using Nat.lt_succ_sqrt'. Strictness x^2 < p comes from s^2 ≠ p: s ∣ p, so s = 1 or s = p. Gotcha: inside the proof, set s := Nat.sqrt p does not rewrite later hypotheses like Nat.sqrt_le' p, so restate them as have h' : s * s = p := ... before rewriting. For p = x^2 + k y^2: the identity x^2 + k y^2 = (x - s y)(x + s y) + (s^2 + k) y^2 gives p ∣ x^2 + k y^2 < (k+1)p, and you then kill the multiples 2p, 3p by parity or mod 3 with omega on emod facts. For (-3/p) use jacobiSym.quadratic_reciprocity_one_mod_four' or quadratic_reciprocity_three_mod_four with χ₄, plus jacobiSym.sq_one (by simp) for J(-1|p)^2.