MeasureTheory.rearrangement_indicator_superlevelSet

lemma rearrangement_indicator_superlevelSet {ε} [TopologicalSpace ε] [ENormedAddMonoid ε]  {f : α → ε} {t : ℝ≥0∞} :    rearrangement ((superlevelSet f t).indicator f) x μ      = (superlevelSet (rearrangement f · μ) t).indicator (rearrangement f · μ) x := by  rw [rearrangement]  simp_rw [distribution_indicator_superlevelSet]  simp only [inf_le_iff]  unfold Set.indicator superlevelSet  simp only [enorm_eq_self, Set.mem_setOf_eq]  split_ifs with h  · rw [lt_rearrangement_iff_lt_distribution] at h    unfold rearrangement    congr with σ    simp [h]  · push Not at h    rw [rearrangement_le_iff_distribution_le] at h    simp [h]