MeasureTheory.rearrangement_const_smul

lemma rearrangement_const_smul {f : α → ℝ≥0∞} {a : ℝ≥0∞} :    rearrangement (a • f) x μ = a * rearrangement f x μ := by  by_cases a_zero : a = 0  · rw [a_zero]    simp  by_cases a_top : a = ⊤  · have : ∞ • f = f.support.indicator (Function.const _ ∞) := by      ext x      unfold Set.indicator Function.support      split_ifs with h      · simp [ENNReal.top_mul h]      · simp_all    rw [a_top, this, rearrangement_indicator_const, ← distribution_zero_eq_measure_support]    unfold Set.indicator    simp only [Set.mem_Iio, enorm_eq_self, Function.const_apply]    split_ifs with hx    · rw [ENNReal.top_mul]      rw [← lt_rearrangement_iff_lt_distribution] at hx      exact hx.ne'    · push Not at hx      rw [← rearrangement_le_iff_distribution_le, nonpos_iff_eq_zero] at hx      rw [hx, mul_zero]  apply le_antisymm  · apply sInf_le    simp only [Set.mem_setOf_eq]    rw [distribution_const_smul (Or.inl a_zero) (Or.inl a_top),      mul_div_assoc, ENNReal.mul_div_cancel a_zero a_top]    apply distribution_rearrangement_le  · apply le_sInf    intro s hs    simp only [Set.mem_setOf_eq] at hs    rw [distribution_const_smul (Or.inl a_zero) (Or.inl a_top)] at hs    calc _      _ ≤ a * rearrangement f (distribution f (s / a) μ) μ := by gcongr      _ ≤ a * (s / a) := by        gcongr        apply rearrangement_distribution_le      _ = s := ENNReal.mul_div_cancel a_zero a_top