∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {s : Set X} {f : X → ℝ} {c : ℝ},
  MeasurableSet s →
    μ s ≠ ⊤ → (∀ x ∈ s, c ≤ f x) → MeasureTheory.IntegrableOn (fun x => f x) s μ → c * μ.real s ≤ ∫ (x : X) in s, f x ∂μ