awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0

Tactic:
have hw (i) (_ : i ∈ t) : w i • p i ≠ 0 → w i ≠ 0 := by simp_all
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
i : ι
h : i ∈ t
⊢ w i • f (p i) ≠ 0 → w i ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0

Tactic:
have hw' (i) (_ : i ∈ t) : w i • f (p i) ≠ 0 → w i ≠ 0 := by simp_all
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
rw :
  (∀ j ∈ {x ∈ t | w x ≠ 0}, p j = ∑ i ∈ t with w i ≠ 0, w i • p i) ↔
    ∀ j ∈ t, w j ≠ 0 → p j = ∑ x ∈ t with w x ≠ 0, w x • p x
h₂ : ∀ i ∈ {x ∈ t | w x ≠ 0}, 0 < w i
h₃ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t with w i ≠ 0, w i) 1
hmem₁ : ∀ i ∈ {x ∈ t | w x ≠ 0}, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i

Tactic:
rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]

Premises used: StrictConvexOn.map_sum_eq_iff, Finset.sum_filter_of_ne
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ (∀ j ∈ {x ∈ t | w x ≠ 0}, p j = ∑ i ∈ t with w i ≠ 0, w i • p i) ↔
    ∀ j ∈ t, w j ≠ 0 → p j = ∑ x ∈ t with w x ≠ 0, w x • p x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, 0 < w i

Tactic:
simp +contextual [(h₀ _ _).lt_iff_ne']

Premises used: LE.le.lt_iff_ne'
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
h₂ h₃ h₄ h₅ : Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ t, w x) 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t with w i ≠ 0, w i) 1

Tactic:
rwa [sum_filter_ne_zero]

Premises used: Finset.sum_filter_ne_zero
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, p i ∈ s

Tactic:
simp +contextual [hmem _ _]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConcaveOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, w j ≠ 0 → p j = ∑ i ∈ t, w i • p i

Tactic:
hf.dual.map_sum_eq_iff' h₀ h₁ hmem

Premises used: OrderDual, StrictConcaveOn.dual, StrictConvexOn.map_sum_eq_iff'
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x : E
t : Finset E
hf : ConvexOn 𝕜 s f
hts : (↑t : Set E) ⊆ s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x
obtain :
  ∀ (w : E → 𝕜) (hw₀ : ∀ y ∈ t, 0 ≤ w y) (hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1)
    (hx :
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        (t.centerMass w _root_.id)),
    f (t.centerMass w _root_.id) ≤ t.sup' ⋯ f
⊢ f x ≤ t.sup' ⋯ f

Tactic:
obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convexHull.1 hx

Premises used: Finset.mem_convexHull, Iff.mp, rfl
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset E
hf : ConvexOn 𝕜 s f
hts : (↑t : Set E) ⊆ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (t.centerMass w _root_.id)
⊢ LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset E
hf : ConvexOn 𝕜 s f
hts : (↑t : Set E) ⊆ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (t.centerMass w _root_.id)
⊢ f (t.centerMass w _root_.id) ≤ t.sup' ⋯ f

Tactic:
exact (hf.map_centerMass_le hw₀ (by positivity) hts).trans
    (centerMass_le_sup hw₀ <| by positivity)

Premises used: ConvexOn.map_centerMass_le, Finset.centerMass_le_sup, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x : E
t : Finset E
hf : ConcaveOn 𝕜 s f
hts : (↑t : Set E) ⊆ s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x
⊢ t.inf' ⋯ f ≤ f x

Tactic:
hf.dual.le_sup_of_mem_convexHull hts hx

Premises used: Finset.inf', WithTop.some, WithTop.untop, ConvexOn.le_sup_of_mem_convexHull, OrderDual, Finset.inf, ConcaveOn.dual, WithTop
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
set :
  let y := t.centerMass w p;
  ∃ i ∈ t, f y ≤ f (p i)
⊢ ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i)

Tactic:
set y := t.centerMass w p

Premises used: Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
rwa rwa₁ rwa₂ rwa₃ : LT.lt.{u_1} (α := 𝕜) 0 (∑ x ∈ t, w x)
⊢ LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)

Tactic:
rwa [sum_filter_ne_zero]

Premises used: Finset.sum_filter_ne_zero
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
⊢ LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)

Tactic:
have hw' : (0 : 𝕜) < ∑ i ∈ t with w i ≠ 0, w i := by rwa [sum_filter_ne_zero]
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)
⊢ ∃ i ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i

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

Premises used: LT.lt.ne', Finset.nonempty_of_sum_ne_zero, Finset.exists_le_of_sum_le
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)
refine : LE.le.{u_4} (α := β) (∑ i ∈ t with w i ≠ 0, w i • f y) (∑ i ∈ t with w i ≠ 0, w i • (f ∘ p) i)
⊢ ∃ i ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i

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

Premises used: LT.lt.ne', Finset.nonempty_of_sum_ne_zero, Finset.exists_le_of_sum_le
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)
rw : f y ≤ t.centerMass w (f ∘ p)
⊢ LE.le.{u_4} (α := β) (∑ i ∈ t with w i ≠ 0, w i • f y) (∑ i ∈ t with w i ≠ 0, 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]

Premises used: Iff.mpr, Finset.sum_smul, inv_smul_smul₀, smul_le_smul_iff_of_pos_left, Finset.centerMass_filter_ne_zero, inv_pos, LT.lt.ne', Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)
⊢ f y ≤ t.centerMass w (f ∘ p)

Tactic:
h.map_centerMass_le hw₀ hw₁ hp

Premises used: ConvexOn.map_centerMass_le
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
hw' : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t with w i ≠ 0, w i)
⊢ f y ≤ t.centerMass w (f ∘ p)

Tactic:
exact h.map_centerMass_le hw₀ hw₁ hp

Premises used: ConvexOn.map_centerMass_le
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
obtain : ∀ (i : ι) (hi : i ∈ {i ∈ t | w i ≠ 0}) (hfi : w i • f y ≤ w i • (f ∘ p) i), ∃ i ∈ t, f y ≤ f (p i)
⊢ ∃ 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
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ {i ∈ t | w i ≠ 0}
hfi : w i • f y ≤ w i • (f ∘ p) i
⊢ i ∈ t ∧ w i ≠ 0

Tactic:
rw [mem_filter] at hi

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
y : E := t.centerMass w p
i : ι
hi : i ∈ {i ∈ t | w i ≠ 0}
hfi : w i • f y ≤ w i • (f ∘ p) i
hi₁ : i ∈ t ∧ w i ≠ 0
⊢ w i • f y ≤ w i • (f ∘ p) i

Tactic:
rw [mem_filter] at hi

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 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)

Tactic:
⟨i, hi.1, (smul_le_smul_iff_of_pos_left <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩

Premises used: smul_le_smul_iff_of_pos_left, Ne.symm, LE.le.lt_of_ne, And.right, And.left, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConvexOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 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)

Tactic:
exact ⟨i, hi.1, (smul_le_smul_iff_of_pos_left <| (hw₀ i hi.1).lt_of_ne hi.2.symm).1 hfi⟩
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
t : Finset ι
h : ConcaveOn 𝕜 s f
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hp : ∀ i ∈ t, p i ∈ s
⊢ ∃ i ∈ t, f (p i) ≤ f (t.centerMass w p)

Tactic:
h.dual.exists_ge_of_centerMass hw₀ hw₁ hp

Premises used: ConvexOn.exists_ge_of_centerMass, ConcaveOn.dual
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x : E
t : Set E
hf : ConvexOn 𝕜 s f
hts : t ⊆ s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (ι : Type) (t_1 : Finset ι) (w : ι → 𝕜) (z : ι → E),
        (∀ i ∈ t_1, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t_1, w i) 1 ∧ (∀ i ∈ t_1, z i ∈ t) ∧ t_1.centerMass w z = x}
    x

Tactic:
rw [_root_.convexHull_eq] at hx

Premises used: convexHull_eq
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
x : E
t : Set E
hf : ConvexOn 𝕜 s f
hts : t ⊆ s
hx :
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (ι : Type) (t_1 : Finset ι) (w : ι → 𝕜) (z : ι → E),
        (∀ i ∈ t_1, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t_1, w i) 1 ∧ (∀ i ∈ t_1, z i ∈ t) ∧ t_1.centerMass w z = x}
    x
obtain :
  ∀ (α : Type) (t_1 : Finset α) (w : α → 𝕜) (p : α → E) (hw₀ : ∀ i ∈ t_1, 0 ≤ w i)
    (hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t_1, w i) 1) (hp : ∀ i ∈ t_1, p i ∈ t), ∃ y ∈ t, f (t_1.centerMass w p) ≤ f y
⊢ ∃ y ∈ t, f x ≤ f y

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

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t_1 : Set E
hf : ConvexOn 𝕜 s f
hts : t_1 ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hp : ∀ i ∈ t, p i ∈ t_1
obtain : ∀ (i : α) (hit : i ∈ t) (Hi : f (t.centerMass w p) ≤ f (p i)), ∃ y ∈ t_1, f (t.centerMass w p) ≤ f y
⊢ ∃ y ∈ t_1, 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)

Premises used: Eq.rec, zero_lt_one, ConvexOn.exists_ge_of_centerMass, Eq.symm
-- Module: Mathlib.Analysis.Convex.Jensen
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup β
inst_5 : LinearOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 E
inst_8 : Module 𝕜 β
inst_9 : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t_1 : Set E
hf : ConvexOn 𝕜 s f
hts : t_1 ⊆ s
α : Type
t : Finset α
w : α → 𝕜
p : α → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
hp : ∀ i ∈ t, p i ∈ t_1
i : α
hit : i ∈ t
Hi : f (t.centerMass w p) ≤ f (p i)
⊢ ∃ y ∈ t_1, f (t.centerMass w p) ≤ f y

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

Premises used: And.intro, Exists.intro