no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.179930
α : Type ?u.179933
β : Type u_3
ι : Type ?u.179939
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x✝⁸ : E
x✝⁷ : x✝⁸ ∈ s
x✝⁶ : E
x✝⁵ : x✝⁶ ∈ s
x✝⁴ x✝³ : 𝕜
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ ↑f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶) ≤ x✝⁴ • ↑f x✝⁸ + x✝³ • ↑f x✝⁶
rw [f.map_add, f.map_smul, f.map_smul]