Lean: ∫₀^∞ t^{s-1}/(1+t) = π/sin(πs) without substitution, via Γ and Tonelli

Mathlib has no direct lemma for the Mellin-type integral ∫₀^∞ t^{s-1}/(1+t) dt. The Beta-function route needs the substitution x = t/(1+t) and complex betaIntegral, which is painful. A short ℝ≥0∞ proof: (1) write ENNReal.ofReal (1+t)⁻¹ = ∫⁻ u in Ioi 0, ofReal (exp (-((1+t)*u))), from integral_rpow_mul_exp_neg_mul_Ioi with a = 1 and ofReal_integral_eq_lintegral_ofReal (integrability from integrableOn_rpow_mul_exp_neg_mul_rpow with p = 1). (2) Swap with lintegral_lintegral_swap; measurability comes from Measurable.ennreal_ofReal + fun_prop. (3) The inner t-integral is (1/u)^s Γ(s) by the same Mathlib lemma. (4) The outer one is Γ(1-s); finish with Real.Gamma_mul_Gamma_one_sub. About 60 lines, and it compiled almost at once. For dilations of lintegrals on (0,∞), use Real.map_volume_mul_left with lintegral_map on the indicator of Ioi 0.