MeasureTheory.measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite'

lemma measure_enorm_mem_eq_volume_rearrangement_mem_of_support_finite' {ε} [TopologicalSpace ε]  [ENormedAddMonoid ε]  {f : α → ε} (hf : AEStronglyMeasurable f μ) (hf' : μ f.support < ∞) {s : Set ℝ≥0∞}  (hs : MeasurableSet s) :    μ {x | ‖f x‖ₑ ∈ s \ {0}} = volume {x | rearrangement f x μ ∈ s \ {0}} := by  apply MeasurableSpace.induction_on_inter    (C := fun s hs ↦ μ {x | ‖f x‖ₑ ∈ s \ {0}} = volume {x | ‖rearrangement f x μ‖ₑ ∈ s \ {0}})    (borel_eq_generateFrom_Ioi ℝ≥0∞) isPiSystem_Ioi _ _ _ _ _ hs  · simp  · intro s hs    rcases hs with ⟨t, ht⟩    rw [← ht]    simp only [Set.mem_Ioi, not_lt_zero, not_false_eq_true, Set.sdiff_singleton_eq_self]    rw [← distribution, ← distribution, distribution_rearrangement_eq_distribution]  · intro s hs h    calc _      _ = μ {x | ‖f x‖ₑ ≠ 0} - μ {x | ‖f x‖ₑ ∈ s \ {0}} := by        rw [← measure_sdiff]        · nth_rw 2 [Set.sdiff_eq]          rw [Set.compl_setOf, ← Set.setOf_and]          congr with x          grind        · simp        · exact AEMeasurable.nullMeasurableSet_preimage hf.enorm (by simp_all)        · rw [← lt_top_iff_ne_top]          apply hf'.trans_le'          gcongr          simp [Function.support]      _ = volume {x | rearrangement f x μ ≠ 0} - volume {x | rearrangement f x μ ∈ s \ {0}} := by        congr        rw [← ENNReal.bot_eq_zero]        simp_rw [← bot_lt_iff_ne_bot]        rw [ENNReal.bot_eq_zero, ← distribution, ← distribution_rearrangement_eq_distribution]        rfl      _ = volume {x | rearrangement f x μ ∈ sᶜ \ {0}} := by        rw [← measure_sdiff]        · nth_rw 1 [Set.sdiff_eq]          rw [Set.compl_setOf, ← Set.setOf_and]          congr with x          grind        · simp        · exact AEMeasurable.nullMeasurableSet_preimage rearrangement_measurable₀.aemeasurable (by simp_all)        · rw [← lt_top_iff_ne_top]          apply hf'.trans_le'          rw [← distribution_zero_eq_measure_support, ← distribution_rearrangement_eq_distribution]          unfold distribution          rw [← ENNReal.bot_eq_zero]          simp_rw [bot_lt_iff_ne_bot]          rw [ENNReal.bot_eq_zero]          gcongr          simp  · intro S hSd hSm hS    calc _      _ = μ (⋃ i, {x | ‖f x‖ₑ ∈ S i \ {0}}) := by        rw [Set.iUnion_setOf]        congr with x        simp      _ = ∑' i, μ ({x | ‖f x‖ₑ ∈ S i \ {0}}) := by        apply measure_iUnion₀        · intro i j hij          unfold Function.onFun          apply Disjoint.aedisjoint          rw [Set.disjoint_iff]          intro x          simp only [Set.mem_sdiff, Set.mem_singleton_iff, enorm_eq_zero, Set.mem_inter_iff,            Set.mem_setOf_eq, Set.mem_empty_iff_false, imp_false, not_and, not_not, and_imp]          intro hi _ hj          exfalso          have := hSd hij          contrapose this          rw [Set.not_disjoint_iff]          use ‖f x‖ₑ, hi, hj        · exact fun i ↦ AEMeasurable.nullMeasurableSet_preimage hf.enorm (by simp_all)      _ = ∑' i,  volume {x | rearrangement f x μ ∈ S i \ {0}} := by        congr with i        exact hS i      _ = volume (⋃ i, {x | rearrangement f x μ ∈ S i \ {0}}) := by        symm        apply measure_iUnion₀        · intro i j hij          unfold Function.onFun          apply Disjoint.aedisjoint          rw [Set.disjoint_iff]          intro x          simp only [Set.mem_sdiff, Set.mem_singleton_iff, Set.mem_inter_iff,            Set.mem_setOf_eq, Set.mem_empty_iff_false, imp_false, not_and, not_not, and_imp]          intro hi _ hj          exfalso          have := hSd hij          contrapose this          rw [Set.not_disjoint_iff]          use ‖rearrangement f x μ‖ₑ, hi, hj        · exact fun i ↦ AEMeasurable.nullMeasurableSet_preimage rearrangement_measurable₀.aemeasurable (by aesop)      _ = volume {x | rearrangement f x μ ∈ (⋃ i, S i) \ {0}} := by        rw [Set.iUnion_setOf]        congr with x        simp