mathlib3

fe2917a4 - feat(number_theory/primes_congruent_one): attempt to golf (#13787)

feat(number_theory/primes_congruent_one): attempt to golf (#13787) As suggested in the reviews of #12595 we try to golf the proof using the bound proved there. This doesn't end up being as much of a golf as hoped due to annoying edge cases, but seems conceptually simpler.