MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement

lemma distribution_comp_eq_distribution_comp_rearrangement {ε} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε}  (hf : AEStronglyMeasurable f μ) (hf' : ∀ σ > 0, distribution f σ μ < ∞) {g : ℝ≥0∞ → ℝ≥0∞} {t : ℝ≥0∞}  (hg : Measurable g) (g_zero : g 0 = 0) :    distribution (fun x ↦ g ‖f x‖ₑ) t μ = distribution (g ∘ (rearrangement f · μ)) t volume := by  by_cases! h : sInf (g ⁻¹' Set.Ioi t) ≠ 0  · rw [← ENNReal.bot_eq_zero, ← bot_lt_iff_ne_bot, ENNReal.bot_eq_zero] at h    apply distribution_comp_eq_distribution_comp_rearrangement' hf hg g_zero    rcases exists_between h with ⟨T, hT, hT'⟩    use T    simp only [hf' _ hT, and_true]    intro s hs    by_contra!    have : sInf (g ⁻¹' Set.Ioi t) ≤ s := by      apply sInf_le      exact this    order  unfold distribution  simp only [enorm_eq_self]  calc _    _ = μ {x | ‖f x‖ₑ ∈ g ⁻¹' Set.Ioi t} := by rfl    _ = volume {s | rearrangement f s μ ∈ g ⁻¹' Set.Ioi t} := by      apply measure_enorm_mem_eq_volume_rearrangement_mem hf (by measurability) (by aesop)      · rw [h]        aesop      intro σ hσ      apply hf'      contrapose! hσ      aesop