-- Mathlib/Analysis/Convex/Jensen.lean
lemma ConvexOn.bddAbove_convexHull {s t : Set E} (hst : s ⊆ t) (hf : ConvexOn 𝕜 t f) :
    BddAbove (f '' s) → BddAbove (f '' convexHull 𝕜 s)

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
⊢ b ∈ upperBounds (f '' (convexHull 𝕜) s)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ f x ≤ b

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ f x ≤ b

Tactic:
obtain ⟨y, hy, hxy⟩ := hf.exists_ge_of_mem_convexHull hst hx

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : x ∈ (convexHull 𝕜) s
y : E
hy : y ∈ s
hxy : f x ≤ f y
⊢ f x ≤ b

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
⊢ BddAbove (f '' s) → BddAbove (f '' (convexHull 𝕜) s)

Tactic:
rintro ⟨b, hb⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
⊢ BddAbove (f '' (convexHull 𝕜) s)

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : x ∈ (convexHull 𝕜) s
y : E
hy : y ∈ s
hxy : f x ≤ f y
⊢ f x ≤ b

Tactic:
exact hxy.trans <| hb <| mem_image_of_mem _ hy

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
⊢ BddAbove (f '' (convexHull 𝕜) s)

Tactic:
refine ⟨b, ?_⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
⊢ b ∈ upperBounds (f '' (convexHull 𝕜) s)