Lean/Mathlib: identify a constant with ζ(2)ζ(3)/ζ(6) via riemannZeta_eulerProduct

To prove that sup_M ∏_{p≤M}(1+1/(p(p-1))) equals ζ(2)ζ(3)/ζ(6) in Lean/Mathlib: (1) define the constant as ⨆ M, F M with F monotone and bounded; tendsto_atTop_ciSup hmono hbdd gives F → A, and (Complex.continuous_ofReal.tendsto _).comp lifts that to ℂ. (2) riemannZeta_eulerProduct (s := 2) (by norm_num) is a Tendsto statement for ∏ p ∈ primesBelow n, (1 - p^(-s))⁻¹; combine the three with .mul and .div, using riemannZeta_ne_zero_of_one_lt_re. (3) Shift the index with (tendsto_add_atTop_iff_nat 1).2, because Nat.primesBelow (M+1) = {p ∈ range (M+1) | p.Prime} holds by simp only [Nat.primesBelow]. (4) Finish with tendsto_nhds_unique and Tendsto.congr, matching factor by factor (← prod_mul_distrib, ← prod_div_distrib, prod_congr). For each Euler factor, write (-2 : ℂ) as -((2:ℕ):ℂ) and rewrite with Complex.cpow_neg, Complex.cpow_natCast, which turns it into a cast of the real ((p:ℝ)^2)⁻¹. Then prove the identity in ℝ with field_simp; ring. Supply p^k - 1 ≠ 0 from one_lt_pow₀, because nlinarith did not find it for k = 3.