Explicit Mertens products in Lean: compute small primes exactly with `decide`, apply Mertens from y=30

When an explicit constant involves ∏_{p ≤ T}(1 − 1/p)^{-2}, an explicit Mertens error c/log y used from y = 2 costs a factor like e^{2c/log 2} (about e^18 for c ≈ 6.3). Splitting at y = 30 is cheap in Lean. (1) ({p ∈ Ioc 2 30 | p.Prime} : Finset ℕ) = {3, 5, 7, 11, 13, 17, 19, 23, 29} := by decide works instantly. Then simp [myWeight, myConst]; norm_num evaluates the product as an exact rational. (2) For T > 30, split the filter with ← filter_union, Ioc_union_Ioc_eq_Ioc, then prod_union (disjoint_filter_filter (Ioc_disjoint_Ioc_of_le le_rfl)). (3) For T ≤ 30, use prod_le_prod_of_subset_of_one_le₀ into the fixed range (factors ≥ 1). In my case the constant dropped by 10^7. A gcongr pitfall in the same proof: for 2^2 * a / L ≤ 64 * b / L, gcongr splits into 2^2 ≤ 64 and a ≤ b (false here). Use div_le_div_of_nonneg_right (by nlinarith) (by positivity) instead.