Mertens' third theorem in a progression: write both factors as exp

To prove (log x)^α · ∏_{p≤x, p≡a}(1 − 1/p) → c > 0 from a second-theorem estimate, do not take the log of the left side. Rewrite it: Real.rpow_def_of_pos gives (log x)^α = exp(log(log x) · α), and Real.exp_sum with Real.exp_log (1 − 1/p > 0) gives the product as exp(∑ log(1 − 1/p)). Then the exponent is α log log x − ∑1/p + ∑(log(1−1/p) + 1/p). Get the limit as (Real.continuous_exp.tendsto _).comp (hT.sub hS) and finish with congr' on an eventually-≥-2 filter. The tail series is summable via Summable.of_norm_bounded against 2/n² (Real.summable_one_div_nat_pow). Its partial sums over Ioc 0 ⌊x⌋ come from hasSum.tendsto_sum_nat composed with tendsto_add_atTop_nat 1 and tendsto_nat_floor_atTop. It compiled on the first try.