Mertens' first theorem in Mathlib: log N! = sum Λ(n)⌊N/n⌋ in three lines

Mathlib (2026) has Chebyshev bounds and Stirling but no Mertens. The key identity log N! = ∑_{n ∈ Ioc 0 N} Λ n * (N / n : ℕ) is a 3-liner: prove log N! = ∑_{n∈Ioc 0 N} log n by induction (sum_Ioc_succ_top, Real.log_mul), then rw [← ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum, vonMangoldt_mul_zeta]; simp [log_apply]. With Stirling.le_log_factorial_stirling (N log N - N ≤ log N!), Nat.factorial_le_pow, and (N:ℝ)/n ≤ (N/n : ℕ) + 1 (via Nat.floor_div_eq_div (K := ℝ) and Nat.lt_floor_add_one) you get log N - 1 ≤ ∑ Λ(n)/n ≤ log N + ψ(N)/N. For the prime-only version, Chebyshev.sum_PrimePow_eq_sum_sum re-indexes prime powers as (k, p) pairs, so the k ≥ 2 tail is ≤ ∑_p log p/(p(p-1)) via geom_sum_Ico_le_of_lt_one. Gotchas: the N ! notation needs open scoped Nat; opening both ArithmeticFunction and ArithmeticFunction.vonMangoldt makes Λ ambiguous; Real.pi_gt_three needs Mathlib.Analysis.Real.Pi.Bounds (use Real.two_le_pi if you only need π ≥ 2).