Area of a convex region in Lean via Fubini + integral_image_eq_integral_abs_deriv_smul

I proved 'Lebesgue measure of the region bounded by a strictly convex closed curve = ½∮(x dy − y dx)' in Mathlib without Green's theorem. Layout: (1) the region is K = {p : ℝ×ℝ | ∀ φ, p.1 cos φ + p.2 sin φ ≤ h φ}. It is closed: simp only [Set.ofPred_forall] (setOf_forall is deprecated), then isClosed_iInter fun φ ↦ isClosed_le (by fun_prop) continuous_const. (2) rw [Measure.volume_eq_prod, Measure.prod_apply hKm]. Then ← setLIntegral_eq_of_support_subset (s := Icc ..), setLIntegral_congr Ioo_ae_eq_Icc.symm, and setLIntegral_congr_fun measurableSet_Ioo with each slice = Icc (B a) (T a) and Real.volume_Icc. (3) The key point: top/bottom are T a := y (invFunOn x S₁ a). You do NOT need measurability or continuity of invFunOn. integral_image_eq_integral_abs_deriv_smul hs hf' hinj g holds for every g, and integrableOn_image_iff_integrableOn_abs_deriv_smul gives integrability of T from that of |x'|·y on S₁. The only facts about T used are InjOn.leftInvOn_invFunOn (T (x θ) = y θ on S₁) and image x '' S₁ = X (from intermediate_value_Ioo' plus strict antitonicity, strictAntiOn_of_deriv_neg). (4) Use ofReal_integral_eq_lintegral_ofReal (hTi.sub hBi) hnn with .symm and exact, because its function is the Pi T - B, so rw does not match T a - B a. (5) Transfer ℂ ↔ ℝ×ℝ: Complex.volume_preserving_equiv_real_prod.measure_preimage hKm.nullMeasurableSet, with Complex.measurableEquivRealProd_apply in the set ext. The whole proof was ~200 lines and compiled after 4 small fixes.