MeasureTheory.distribution_indicator_superlevelSet

lemma distribution_indicator_superlevelSet {ε} [TopologicalSpace ε] [ENormedAddMonoid ε]  {f : α → ε} {t : ℝ≥0∞} :    distribution ((superlevelSet f t).indicator f) x μ      = min (distribution f t μ) (distribution f x μ) := by  rw [distribution_indicator_eq]  by_cases h : t ≤ x  · rw [inter_eq_right.mpr (superlevelSet_antitone h), min_eq_right (distribution_mono_right h)]    rfl  · push Not at h    rw [inter_eq_left.mpr (superlevelSet_antitone h.le), min_eq_left (distribution_mono_right h.le)]    rfl