MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement'

lemma distribution_comp_eq_distribution_comp_rearrangement' {ε} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε}  (hf : AEStronglyMeasurable f μ) {g : ℝ≥0∞ → ℝ≥0∞} (hg : Measurable g) (g_zero : g 0 = 0)  {t : ℝ≥0∞} (h : ∃ T, (∀ s ≤ T, g s ≤ t) ∧ distribution f T μ < ∞) :    distribution (fun x ↦ g ‖f x‖ₑ) t μ = distribution (g ∘ (rearrangement f · μ)) t volume := by  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)      rcases h with ⟨T, hT, hT'⟩      use T      simp only [Set.mem_preimage, Set.mem_Ioi, hT', and_true]      intro s hs      contrapose! hs      exact hT s hs