∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {a b : ENNReal},
  a ≠ ⊤ →
    b ≠ ⊤ → ∀ {X : α → ENNReal}, AEMeasurable X μ → (∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.Integrable X μ