MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem'

lemma measure_enorm_mem_eq_volume_rearrangement_mem' {ε} [TopologicalSpace ε] [ENormedAddMonoid ε]  {f : α → ε} (hf : AEStronglyMeasurable f μ) {s : Set ℝ≥0∞}  (hs : MeasurableSet s) (zero_notin_s : 0 ∉ s) (h : ∃ T, (∀ t ∈ s, T < t) ∧ distribution f T μ < ∞) :    μ {x | ‖f x‖ₑ ∈ s} = volume {x | rearrangement f x μ ∈ s} := by  rcases h with ⟨T, hT, hT'⟩  have hμ : {x | ‖f x‖ₑ ∈ s} = {x | ‖(superlevelSet f T).indicator f x‖ₑ ∈ s} := by    ext x    unfold superlevelSet Set.indicator    aesop  have hvolume : {x | rearrangement f x μ ∈ s}      = {x | (superlevelSet (rearrangement f · μ) T).indicator (rearrangement f · μ) x ∈ s} := by    ext x    unfold superlevelSet Set.indicator    aesop  rw [hμ, hvolume]  rw [measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite (μ := μ) _ _ hs zero_notin_s]  · congr with x    rw [rearrangement_indicator_superlevelSet]  · exact hf.indicator₀ (nullMeasurableSet_superlevelSet hf)  · rw [← distribution_zero_eq_measure_support, distribution_indicator_superlevelSet]    exact min_lt_of_left_lt hT'