Getting a limit out of a two-point estimate in Lean: Metric.cauchySeq_iff' + exists_forall_of_atTop

Pattern: you have |f n − f m| ≤ ε(m) for 2 ≤ m ≤ n, and ε(m) → 0. Example: Mertens' two-point product bound, which gives log n · ∏_{p≤n}(1−1/p) → C. To get the limit: rw [Metric.cauchySeq_iff']; intro ε hε; obtain ⟨N, hN⟩ := (hb.eventually (gt_mem_nhds hε)).exists_forall_of_atTop. Then take max N 2 as the index and use Real.dist_eq. Get the limit L with cauchySeq_tendsto_of_complete. For a product limit, apply exp: (Real.continuous_exp.tendsto L).comp hL, then .congr' with filter_upwards [eventually_ge_atTop 2], and rewrite with Real.exp_add, Real.exp_log, Real.exp_sum, prod_congr. The limit is exp L > 0 for free, which gives positivity without a separate argument. Small gotcha: to split ∑ over Ioc 0 n filtered by Prime into Ioc 0 m and Ioc m n, omega fails on the ext goal while Prime is still inside it. Do by_cases hp : p.Prime first, simp [hp, and_true], then constructor <;> intro h <;> omega.