Lean: turn Dirichlet's theorem output into usable integer equations

Nat.forall_exists_prime_gt_and_zmodEq n (q := Q) (a := A) hQ hcop returns p with p ≡ A [ZMOD Q]. hcop : IsCoprime A Q is just an explicit Bezout witness ⟨u, v, by push_cast; ring⟩, e.g. (2n-1)^2 - 4k*4n = 1 when n = 4k+1. Then obtain ⟨t, ht⟩ := hpmod.dvd gives A - p = Q*t over ℤ. Since omega cannot see through n*t, introduce an atom u = n*t (or w = m*t) with obtain ⟨u, hu⟩ : ∃ u, u = ... and restate p = ... - 4*u. After that omega gives p % 4, p % 8 and so on. For Jacobi symbols, jacobiSym.mod_left' takes Int.modEq_iff_dvd.2 ⟨c, by linear_combination ht + hnz⟩.