Lean: bound ∑_{q≤M} 1/φ(q) ≤ 2(1+log M) via powerset expansion of q/φ(q)

Route that avoids squarefree-divisor bijections and φ of products: (1) q/φ(q) = ∏_{p∈q.primeFactors}(1-p⁻¹)⁻¹ (from Nat.totient_eq_mul_prod_factors), rewrite each factor as 1 + 1/(p-1), then Finset.prod_one_add turns it into ∑_{t ∈ primeFactors.powerset} ∏_{p∈t} 1/(p-1). (2) Swap with the q-sum using Finset.sum_comm' with the condition q ∈ Icc 1 M ∧ t ⊆ q.primeFactors ↔ (∏ p ∈ t, p) ∣ q ∧ q ∈ Icc 1 M ∧ t ⊆ primes ≤ M; forward direction is Finset.prod_primes_dvd (needs Nat.Prime.prime), backward is dvd_prod_of_mem + Nat.mem_primeFactors. Put subset_iff in the simp set, otherwise membership in a filtered range unfolds to List.Mem and anonymous constructors fail. (3) Inner sum over multiples of d is (1/d)·harmonic ≤ (1/d)(1+log M); prod_one_add backwards gives ∏_{p≤M}(1+1/(p(p-1))). (4) Bound the product by 2: rewrite (range 31).filter Nat.Prime = {2,3,5,...,29} by decide, then norm_num (doing simp [prod_range_succ] with 31 if n.Prime terms timed out); above 30 induct with invariant ≤ 2(M-1)/M, since (M-1)/M·(1+1/(M(M+1))) ≤ M/(M+1) ⟺ M³-1 ≤ M³. Precedence gotcha: ∏ p ∈ t, f p * c puts c inside the product; parenthesise.