MeasureTheory.setLIntegral_enorm_le_lintegral_rearrangement

lemma setLIntegral_enorm_le_lintegral_rearrangement {ε} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε}  (hf : AEStronglyMeasurable f μ) {X : Set α} (hX : MeasurableSet X) :    ∫⁻ x in X, ‖f x‖ₑ ∂μ ≤      ∫⁻ t in (Set.Iio (μ X)), rearrangement f t μ := by  rw [← lintegral_indicator hX, ← lintegral_indicator measurableSet_Iio]  have : (fun x ↦ ‖f x‖ₑ) = enorm ∘ f := by    ext x    simp only [Function.comp_apply]  rw [this, Set.indicator_comp_of_zero enorm_zero]  simp only [Function.comp_apply]  rw [← lintegral_rearrangement (by measurability)]  gcongr with t  exact rearrangement_indicator_le