MeasureTheory.AEStronglyMeasurable.trunc_ton

@[fun_prop]lemma AEStronglyMeasurable.trunc_ton {f : α → E₁}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    (hf : AEStronglyMeasurable f μ) (tc : ToneCouple) :    AEStronglyMeasurable (fun a : ℝ≥0∞ × α ↦ (MeasureTheory.trunc f (tc.ton a.1)) a.2)      ((volume.restrict (Ioi 0)).prod (μ.restrict f.support)) := by  let A := {(s, x) : ℝ≥0∞ × α | ‖f x‖ₑ ≤ tc.ton s}  have : (fun z : ℝ≥0∞ × α ↦ (MeasureTheory.trunc f (tc.ton z.1)) z.2) =      Set.indicator A (fun z : ℝ≥0∞ × α ↦ f z.2) := by    ext z; simp [MeasureTheory.trunc, indicator, A]  rw [this]  exact (aestronglyMeasurable_indicator_iff₀ (indicator_ton_measurable (hf.restrict) _)).mpr    hf.restrict.comp_snd.restrict