MeasureTheory.distribution_rearrangement_le

lemma distribution_rearrangement_le : distribution f (rearrangement f x μ) μ ≤ x := by  by_cases hx : rearrangement f x μ = ⊤;  · aesop  · -- By definition of `rearrangement`, we know that for any ε > 0, `distribution f (rearrangement f x μ + ε) μ ≤ x`.    have h_eps : ∀ ε > 0, distribution f (rearrangement f x μ + ε) μ ≤ x := by      intro ε ε_pos      have := exists_lt_of_csInf_lt (by contrapose! hx; simp_all [rearrangement]) (ENNReal.lt_add_right hx ε_pos.ne')      rcases this with  ⟨σ, hσ₁, hσ₂⟩      exact le_trans (distribution_mono_right hσ₂.le) hσ₁;    have h_lim : Filter.Tendsto (fun ε => distribution f (rearrangement f x μ + ε) μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (distribution f (rearrangement f x μ) μ)) := by      have h_lim : ContinuousWithinAt (fun ε => distribution f (rearrangement f x μ + ε) μ) (Set.Ioi 0) 0 := by        have h_lim : ContinuousWithinAt (fun ε => distribution f ε μ) (Set.Ioi (rearrangement f x μ)) (rearrangement f x μ) :=          continuousWithinAt_distribution (rearrangement f x μ);        rw [ContinuousWithinAt] at *;        convert! h_lim.comp (show Filter.Tendsto (fun ε : ℝ≥0∞ => rearrangement f x μ + ε) (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin (rearrangement f x μ) (Set.Ioi (MeasureTheory.rearrangement f x μ))) from ?_) using 2;        · rw [ add_zero ];        · rw [ tendsto_nhdsWithin_iff ];          simp_all only [gt_iff_lt, Set.mem_Ioi]          constructor          · exact tendsto_nhdsWithin_of_tendsto_nhds (Continuous.tendsto' (by continuity) _ _ (by simp));          · filter_upwards [ self_mem_nhdsWithin ] with n hn using ENNReal.lt_add_right hx hn.ne';      simpa using h_lim.tendsto    exact le_of_tendsto h_lim (Filter.eventually_of_mem self_mem_nhdsWithin fun ε hε => h_eps ε hε)