refine (integrableOn_union.mpr ⟨?_, hs.mono ha' le_rfl⟩).mono Ici_subset_Icc_union_Ici le_rfl
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Ici a) μ
case intro
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ
s : Set X
hsl : s ∈ atTop
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Ici a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≥ a', b ∈ s
⊢ IntegrableOn f (Icc a a') μ