MeasureTheory.lintegral_comp_rearrangement'

lemma lintegral_comp_rearrangement' {ε} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : α → ε}  (hf : AEStronglyMeasurable f μ) {g : ℝ≥0∞ → ℝ≥0∞} (hg : Measurable g) (g_zero : g 0 = 0)  (hg' : ∀ t > 0, distribution f t μ = ∞ → ∃ S > 0, ∀ y > t, S < g y) :    ∫⁻ x, g ‖f x‖ₑ ∂μ = ∫⁻ t, g (rearrangement f t μ) := by  set T := sInf {σ | distribution f σ μ < ∞}  rw [lintegral_eq_lintegral_distribution _ (by fun_prop)]  symm  rw [lintegral_eq_lintegral_distribution _ (by fun_prop)]  symm  by_cases hT : T = 0  · congr with t    apply distribution_comp_eq_distribution_comp_rearrangement hf _ hg g_zero    unfold T at hT    rw [← ENNReal.bot_eq_zero, sInf_eq_bot] at hT    intro σ hσ    rcases hT σ hσ with ⟨s, hs, hsσ⟩    exact hs.trans_le' (distribution_mono_right hsσ.le)  unfold T at hT  rw [← ENNReal.bot_eq_zero, sInf_eq_bot] at hT  simp only [bot_eq_zero', Set.mem_setOf_eq, not_forall, not_exists,    not_and, not_lt] at hT  simp_rw [← not_lt, imp_not_comm, not_lt, top_le_iff] at hT  rcases hT with ⟨u, u_pos, hu⟩  rcases exists_between u_pos with ⟨t, t_pos, ht⟩  have ht := hu t ht  have hS : ∃ S > 0, distribution (fun x ↦ g ‖f x‖ₑ) S μ = ∞ := by    rcases hg' t t_pos ht with ⟨S, S_pos, hS⟩    use S, S_pos    rw [← top_le_iff, ← ht]    unfold distribution    gcongr 2 with x    intro h    simp only [enorm_eq_self]    exact hS _ h  have hS' : ∃ S > 0, distribution (fun t ↦ g (rearrangement f t μ)) S volume = ∞ := by    rcases hg' t t_pos ht with ⟨S, S_pos, hS⟩    use S, S_pos    rw [← top_le_iff, ← ht, ← distribution_rearrangement_eq_distribution]    unfold distribution    gcongr 2 with x    intro h    simp only [enorm_eq_self]    exact hS _ h  convert (Eq.refl ∞)  · rw [eq_top_iff]    rcases hS with ⟨S, S_pos, hS⟩    calc _      _ = ∫⁻ t in Set.Iio S, ⊤ := by        rw [lintegral_const]        simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter]        rw [ENNReal.volume_Iio, ENNReal.top_mul S_pos.ne']      _ = ∫⁻ t in Set.Iio S, distribution (fun x ↦ g ‖f x‖ₑ) t μ := by        apply setLIntegral_congr_fun measurableSet_Iio        intro x hx        simp only        symm        rw [eq_top_iff, ← hS]        apply distribution_mono_right hx.le      _ ≤ ∫⁻ t, distribution (fun x ↦ g ‖f x‖ₑ) t μ := by        apply setLIntegral_le_lintegral  · rw [eq_top_iff]    rcases hS' with ⟨S, S_pos, hS⟩    calc _      _ = ∫⁻ t in Set.Iio S, ⊤ := by        rw [lintegral_const]        simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter]        rw [ENNReal.volume_Iio, ENNReal.top_mul S_pos.ne']      _ = ∫⁻ t in Set.Iio S, distribution (fun t ↦ g (rearrangement f t μ)) t volume := by        apply setLIntegral_congr_fun measurableSet_Iio        intro x hx        simp only        symm        rw [eq_top_iff, ← hS]        apply distribution_mono_right hx.le      _ ≤ ∫⁻ t, distribution (fun t ↦ g (rearrangement f t μ)) t volume := by        apply setLIntegral_le_lintegral