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) (inf_not_mem : sInf s ∉ s)  (hs' : ∀ t ∈ s, distribution f t μ < ∞) :    μ {x | ‖f x‖ₑ ∈ s} = volume {x | rearrangement f x μ ∈ s} := by  by_cases s_nonempty : s = ∅  · rw [s_nonempty]    simp  simp_rw [← Set.nonempty_iff_ne_empty] at s_nonempty  have s_bddBelow : BddBelow s := by simp  rcases exists_seq_tendsto_sInf s_nonempty s_bddBelow with ⟨u, antitone_u, tendsto_u, hus⟩  have hμ : {x | ‖f x‖ₑ ∈ s} = ⋃ n, {x | ‖(superlevelSet f (u n)).indicator f x‖ₑ ∈ s} := by    ext x    unfold superlevelSet Set.indicator    simp only [Set.mem_setOf_eq, Set.mem_iUnion]    constructor    · intro hfs      have : ∃ i, u i < ‖f x‖ₑ := by        refine iInf_lt_iff.mp ?_        rw [iInf_eq_of_tendsto antitone_u tendsto_u]        apply lt_of_le_of_ne (sInf_le hfs)        grind      rcases this with ⟨i, hi⟩      use i      split_ifs      use hfs    · aesop  have hvolume : {x | rearrangement f x μ ∈ s}      = ⋃ n, {x | (superlevelSet (rearrangement f · μ) (u n)).indicator (rearrangement f · μ) x ∈ s} := by    ext x    unfold superlevelSet Set.indicator    simp only [Set.mem_setOf_eq, Set.mem_iUnion]    constructor    · intro hfs      have : ∃ i, u i < rearrangement f x μ := by        refine iInf_lt_iff.mp ?_        rw [iInf_eq_of_tendsto antitone_u tendsto_u]        apply lt_of_le_of_ne (sInf_le hfs)        grind      rcases this with ⟨i, hi⟩      use i      simp only [enorm_eq_self]      split_ifs      use hfs    · aesop  rw [hμ, hvolume, Monotone.measure_iUnion, Monotone.measure_iUnion]  · congr with i    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 (hs' (u i) (hus i))  · intro n m hmn    simp only    unfold Set.indicator    intro x    simp only [Set.mem_setOf_eq]    split_ifs with hn hm    · exact id    · exfalso      unfold superlevelSet at hn hm      simp only [enorm_eq_self, Set.mem_setOf_eq, not_lt] at hn hm      have := antitone_u hmn      order    · simp [zero_notin_s]    · exact id  · intro n m hmn    simp only    unfold Set.indicator    intro x    simp only [Set.mem_setOf_eq]    split_ifs with hn hm    · exact id    · exfalso      unfold superlevelSet at hn hm      simp only [Set.mem_setOf_eq, not_lt] at hn hm      have := antitone_u hmn      order    · simp [zero_notin_s]    · exact id