-- Mathlib/Analysis/Convex/Jensen.lean
/-- **Maximum principle** for convex functions. If a function `f` is convex on the convex hull of
`s`, then the eventual maximum of `f` on `convexHull 𝕜 s` lies in `s`. -/
lemma ConvexOn.exists_ge_of_mem_convexHull {t : Set E} (hf : ConvexOn 𝕜 s f) (hts : t ⊆ s)
    (hx : x ∈ convexHull 𝕜 t) : ∃ y ∈ t, f x ≤ f y

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 𝕜 β
s : Set E
f : E → β
x : E
t : Set E
hf : ConvexOn 𝕜 s f
hts : t ⊆ s
hx : x ∈ (convexHull 𝕜) t
⊢ ∃ y ∈ t, f x ≤ f y

Tactic:
rw [_root_.convexHull_eq] at hx

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
x : E
t : Set E
hf : ConvexOn 𝕜 s f
hts : t ⊆ s
hx : x ∈ {x | ∃ ι t_1 w z, (∀ i ∈ t_1, 0 ≤ w i) ∧ ∑ i ∈ t_1, w i = 1 ∧ (∀ i ∈ t_1, z i ∈ t) ∧ t_1.centerMass w z = x}
⊢ ∃ y ∈ t, f x ≤ f y

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 𝕜 β
s : Set E
f : E → β
x : E
t : Set E
hf : ConvexOn 𝕜 s f
hts : t ⊆ s
hx : x ∈ {x | ∃ ι t_1 w z, (∀ i ∈ t_1, 0 ≤ w i) ∧ ∑ i ∈ t_1, w i = 1 ∧ (∀ i ∈ t_1, z i ∈ t) ∧ t_1.centerMass w z = x}
⊢ ∃ y ∈ t, f x ≤ f y

Tactic:
obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx

Result:
case intro.intro.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 𝕜 β
s : Set E
f : E → β
t✝ : Set E
hf : ConvexOn 𝕜 s f
hts : t✝ ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hp : ∀ i ∈ t, p i ∈ t✝
⊢ ∃ y ∈ t✝, f (t.centerMass w p) ≤ f y

Proof state:
case intro.intro.intro.intro.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 𝕜 β
s : Set E
f : E → β
t✝ : Set E
hf : ConvexOn 𝕜 s f
hts : t✝ ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hp : ∀ i ∈ t, p i ∈ t✝
i : α
hit : i ∈ t
Hi : f (t.centerMass w p) ≤ f (p i)
⊢ ∃ y ∈ t✝, f (t.centerMass w p) ≤ f y

Tactic:
exact ⟨p i, hp i hit, Hi⟩

Result:
no goals

Proof state:
case intro.intro.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 𝕜 β
s : Set E
f : E → β
t✝ : Set E
hf : ConvexOn 𝕜 s f
hts : t✝ ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hp : ∀ i ∈ t, p i ∈ t✝
⊢ ∃ y ∈ t✝, f (t.centerMass w p) ≤ f y

Tactic:
obtain ⟨i, hit, Hi⟩ := hf.exists_ge_of_centerMass hw₀ (hw₁.symm ▸ zero_lt_one)
  fun i hi ↦ hts (hp i hi)

Result:
case intro.intro.intro.intro.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 𝕜 β
s : Set E
f : E → β
t✝ : Set E
hf : ConvexOn 𝕜 s f
hts : t✝ ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
hp : ∀ i ∈ t, p i ∈ t✝
i : α
hit : i ∈ t
Hi : f (t.centerMass w p) ≤ f (p i)
⊢ ∃ y ∈ t✝, f (t.centerMass w p) ≤ f y