MeasureTheory.distribution_indicator_superlevelSet_compl

lemma distribution_indicator_superlevelSet_compl {ε} [TopologicalSpace ε] [ENormedAddMonoid ε]  {f : α → ε} (hf : AEStronglyMeasurable f μ) {t : ℝ≥0∞} (ht : distribution f t μ ≠ ∞) :    distribution ((superlevelSet f t)ᶜ.indicator f) x μ      = distribution f x μ - distribution f t μ := by  rw [distribution_indicator_eq]  by_cases h : t ≤ x  · rw [tsub_eq_zero_of_le (distribution_mono_right h), ← measure_empty (μ := μ)]    rw [← sdiff_eq_compl_inter, sdiff_eq_empty.mpr (superlevelSet_antitone h)]  · push Not at h    rw [← sdiff_eq_compl_inter,      measure_sdiff (superlevelSet_antitone h.le) (nullMeasurableSet_superlevelSet hf) ht]    rfl