no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.21381
β : Type u_3
ι : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : ConvexOn 𝕜 s f
h₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
h₁ : ∑ i in t, w i = 1
hmem : ∀ (i : ι), i ∈ t → p i ∈ s
⊢ f (∑ i in t, w i • p i) ≤ ∑ i in t, w i • f (p i)
simpa only [centerMass, h₁, inv_one, one_smul] using
  hf.map_centerMass_le h₀ (h₁.symm ▸ zero_lt_one) hmem