no goals
α : Type u_2
E : Type u_1
F : Type ?u.1216893
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : MeasureTheory.Measure α
s : Set E
t : Set α
f : α → E
g : E → ℝ
C : ℝ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
h0 : ↑↑μ t ≠ 0
ht : ↑↑μ t ≠ ⊤
hfs : ∀ᵐ (x : α) ∂Measure.restrict μ t, f x ∈ s
hfi : IntegrableOn f t
hgi : IntegrableOn (g ∘ f) t
⊢ (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.fst ∈ s ∧ p.snd ≤ g p.fst}
simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
  hg.neg.set_average_mem_epigraph hgc.neg hsc h0 ht hfs hfi hgi.neg