no goals
α : Type u_1
E : Type u_2
F : Type ?u.228473
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s✝ : Set E
inst✝ : IsFiniteMeasure μ
f : α → E
s : Set α
hs : NullMeasurableSet s
hs₀ : ↑↑μ s ≠ 0
hsc₀ : ↑↑μ (sᶜ) ≠ 0
hfi : Integrable f
⊢ (⨍ (x : α), f x ∂μ) ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)
simpa only [union_compl_self, restrict_univ] using
  average_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _)
    (measure_ne_top _ _) hfi.integrableOn hfi.integrableOn