theorem integrableOn_toReal {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {g : α → ENNReal} (t : Set α) (hm : m ≤ m0) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg_int_finite : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫⁻ (a : α) in t, g a ∂μ ≠ ⊤) : MeasureTheory.IntegrableOn (fun (x : α) => (g x).toReal) t μ