MeasureTheory.sSup_rearrangement

lemma sSup_rearrangement :    ⨆ t > 0, rearrangement f t μ = rearrangement f 0 μ := by  have h := continuousWithinAt_rearrangement (x := 0) (f := f) (μ := μ)  rw [← continuousWithinAt_Ioi_iff_Ici] at h  rw [iSup_eq_of_forall_le_of_forall_lt_exists_gt]  · intro i    simp only [gt_iff_lt, iSup_le_iff]    intro hi    exact rearrangement_antitone' hi.le  · intro w hw    have := (h.eventually (lt_mem_nhds hw)).and self_mem_nhdsWithin    obtain ⟨t, ht₁, ht₂⟩ := this.exists    use t    aesop