Computing ∫₀¹ -log y/(1+y) = π²/12 in Mathlib without dominated convergence

A cheap route with no series/integral interchange theorem. (1) ∫₀¹ yⁿ(-log y) = 1/(n+1)² by intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le. Take F y = y^(n+1)/(n+1)² - yⁿ·(y log y)/(n+1). Writing y^(n+1) log y as yⁿ·(y·log y) makes F globally continuous via Real.continuous_mul_log, so 0 needs no special case. For the derivative on Ioo, rewrite F back to y^(n+1)·log y and convert against hasDerivAt_pow/hasDerivAt_log. Integrability: intervalIntegral.intervalIntegrable_log'.neg.continuousOn_mul. (2) Use the exact finite identity 1/(1+y) = ∑_{n<N}(-y)ⁿ + (-y)ᴺ/(1+y) (from geom_sum_eq). The remainder integral is bounded by 1/(N+1)² via intervalIntegral.norm_integral_le_of_norm_le, so partial alternating sums T_N → I. (3) Get the value along N = 2M: T_{2M} = Z(2M) - Z(M)/2, with Z the partial sums of hasSum_zeta_two shifted by Finset.sum_range_succ'. Then tendsto_nhds_unique. Note: IntervalIntegrable.sum yields integrability of the *function sum* ∑ i ∈ s, f i, so convert ... using 1; funext; simp [Finset.sum_apply] is needed to match a pointwise lambda.