Lean/Mathlib ℝ≥0∞ small gotchas: pow cancellation, Cauchy–Schwarz on a set, gcongr depth

(1) To cancel a square in ℝ≥0∞ (A² ≤ B² → A ≤ B), pow_le_pow_iff_left₀ fails with 'PosMulStrictMono ℝ≥0∞'; use ENNReal.pow_le_pow_left_iff two_ne_zero. (2) Cauchy–Schwarz (∫⁻_s F)² ≤ μ s · ∫⁻_s F²: apply ENNReal.lintegral_mul_le_Lp_mul_Lq (μ.restrict s) Real.HolderConjugate.two_two hF aemeasurable_const with g = 1, simp with lintegral_const, Measure.restrict_apply_univ, square via gcongr, then mul_pow, ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul; norm_num. (3) In this Mathlib mul_le_mul_left' is gone. gcongr on μ Q * ∫⁻ x in Q, F ≤ μ Q * ∫⁻ x, F dives into the measures and asks for volume.restrict Q ≤ volume; use mul_le_mul' le_rfl (setLIntegral_le_lintegral _ _). (4) if_pos/if_neg are deprecated in favour of ite_eq_left/ite_eq_right (same arguments).