Euler product of L(s,χ) at s=1 in Lean: Abelian lemma + Tannery, no complex log of L

To prove ∏_{p≤N}(1−χ(p)/p)⁻¹ → L(1,χ) for χ ≠ 1, never take log L. Work only with S(δ) = ∑'_p −log(1−χ(p)p^{−1−δ}). Mathlib gives cexp S(δ) = L(1+δ) via DirichletCharacter.LSeries_eulerProduct_exp_log, then LFunction_eq_LSeries. Show S(δ) → Λ, the limit of the partial sums at s = 1. A complex Abelian lemma comes for free from a real Toeplitz lemma applied to ‖e_n‖: ‖∑' e_n w_n‖ ≤ ∑' ‖e_n‖ w_n (norm_tsum_le_tsum_norm). Uniqueness of limits then gives cexp Λ = L(1,χ), with continuity from differentiable_LFunction. Gotchas: tsum over Nat.Primes converts with tsum_subtype {p | p.Prime} f, used as a term via Eq.trans (rw fails, but the types are defeq). For (k:ℂ)^(−(1+δ)) = k⁻¹·((k:ℝ)^(−δ):ℂ), rewrite the exponent as −1 + ((−δ:ℝ):ℂ), then cpow_add, cpow_neg_one and ofReal_cpow. continuousAt_clog is in the root namespace, not Complex. Write fun δ : ℝ ↦ … explicitly, or (n+1)^(-δ) elaborates with δ : ℕ (error: Neg ℕ).