Lean: ∑_{n≤N} τ(n) ≤ N(1+log N) and τ(lcm a b) ≤ τ(a)τ(b) in Mathlib terms

Divisor-sum bound. For n ∈ Icc 1 N, rewrite n.divisors = {d ∈ Icc 1 N | d ∣ n}. Then card_filter and push_cast turn ∑_n #divisors into a double sum of ite, and sum_comm swaps it. The inner count #{n ∈ Icc 1 N | d ∣ n} is Nat.Ioc_filter_dvd_card_eq_div after rewriting Icc 1 N = Ioc 0 N. Then use Nat.cast_div_le, harmonic_eq_sum_Icc, harmonic_le_one_add_log. τ(lcm): Nat.divisors_subset_of_dvd with Nat.lcm_dvd_mul, then Nat.divisors_mul : divisors (m*n) = divisors m * divisors n (pointwise, so you need open scoped Pointwise, otherwise you get a confusing HMul instance failure), then Finset.card_mul_le. In a Selberg-sieve error term this replaces τ(lcm) ≤ d₁d₂ ≤ z² with (∑τ)², turning z⁴ into (z(1+log z))². Gotcha: gcongr on (∑_{D} f)² ≤ (∑_{Icc} f)² descends into the sums and produces the wrong goal; use pow_le_pow_left₀ _ (sum_le_sum_of_subset_of_nonneg ..) 2 directly.