MeasureTheory.AEStronglyMeasurable.truncCompl_ton

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