-- Mathlib/Analysis/Convex/Jensen.lean
/-- If a function `f` is convex on `s`, then the value it takes at some center of mass of points of
`s` is less than the value it takes on one of those points. -/
lemma ConvexOn.exists_ge_of_centerMass {t : Finset ι} (h : ConvexOn 𝕜 s f)
    (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : 0 < ∑ i ∈ t, w i) (hp : ∀ i ∈ t, p i ∈ s) :
    ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) t
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i ∈ t, f y ≤ f (p i)

Tactic:
rw [mem_filter] at hi

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ t ∧ w i ≠ 0
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i ∈ t, f y ≤ f (p i)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i
⊢ ∃ i ∈ filter (fun i => w i ≠ 0) t, w i • f y ≤ w i • (f ∘ p) i

Tactic:
refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i
⊢ ∑ i ∈ filter (fun i => w i ≠ 0) t, w i • f y ≤ ∑ i ∈ filter (fun i => w i ≠ 0) t, w i • (f ∘ p) i

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ ∃ i ∈ filter (fun i => w i ≠ 0) t, w i • f y ≤ w i • (f ∘ p) i

Tactic:
have hw' : (0 : 𝕜) < ∑ i ∈ t with w i ≠ 0, w i := by rwa [sum_filter_ne_zero]

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i
⊢ ∃ i ∈ filter (fun i => w i ≠ 0) t, w i • f y ≤ w i • (f ∘ p) i

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i

Tactic:
rwa [sum_filter_ne_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i
⊢ f y ≤ t.centerMass w (f ∘ p)

Tactic:
exact h.map_centerMass_le hw₀ hw₁ hp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i
⊢ ∑ i ∈ filter (fun i => w i ≠ 0) t, w i • f y ≤ ∑ i ∈ filter (fun i => w i ≠ 0) t, w i • (f ∘ p) i

Tactic:
rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ←
  centerMass, centerMass_filter_ne_zero]

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : 0 < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i
⊢ f y ≤ t.centerMass w (f ∘ p)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
⊢ ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i)

Tactic:
set y := t.centerMass w p

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ ∃ i ∈ t, f y ≤ f (p i)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ ∃ i ∈ t, f y ≤ f (p i)

Tactic:
obtain ⟨i, hi, hfi⟩ : ∃ i ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i := by
  have hw' : (0 : 𝕜) < ∑ i ∈ t with w i ≠ 0, w i := by rwa [sum_filter_ne_zero]
  refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_
  rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ←
    centerMass, centerMass_filter_ne_zero]
  exact h.map_centerMass_le hw₀ hw₁ hp

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ t, w i
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) t
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ ∃ i ∈ t, f y ≤ f (p i)