awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (hypothesis)
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
⊢ 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
have hw' : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ 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
have 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
Tactic: rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ 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
have h₂ : ∀ i ∈ {x ∈ t | w x ≠ 0}, 0 < w i
Tactic: rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ 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
have h₃ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t with w i ≠ 0, w i) 1
Tactic: rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ 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
have hmem₁ : ∀ i ∈ {x ∈ t | w x ≠ 0}, p i ∈ s
Tactic: rw [← sum_filter_of_ne hw, ← sum_filter_of_ne hw', hf.map_sum_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ f x ≤ t.sup' ⋯ f
have 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' sorry f
Tactic: obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convexHull.1 hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (hypothesis)
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 ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i
have hw' : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
have 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)
Tactic: refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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)
⊢ 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)
have rw : f y ≤ t.centerMass w (f ∘ p)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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 ∈ t, f y ≤ f (p i)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (hypothesis)
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, f y ≤ f (p i)
have hi₁ : i ∈ t ∧ w i ≠ 0
Tactic: rw [mem_filter] at hi
Cleared hypotheses: hi, hfi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (hypothesis)
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
⊢ ∃ y ∈ t, f x ≤ f y
have 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
Tactic: rw [_root_.convexHull_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ ∃ y ∈ t, f x ≤ f y
have 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
Tactic: obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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
⊢ ∃ y ∈ t_1, f (t.centerMass w p) ≤ f y
have obtain : ∀ (i : α) (hit : i ∈ t) (Hi : f (t.centerMass w p) ≤ f (p i)), ∃ 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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (hypothesis)
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 y z : E
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ [x -[𝕜] y]
⊢ f z ≤ max (f x) (f y)
have hz₁ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {x, y} : Set E) z
Tactic: rw [← convexHull_pair] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (hypothesis)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup β
inst_4 : LinearOrder β
inst_5 : IsOrderedAddMonoid β
inst_6 : Module 𝕜 β
inst_7 : IsStrictOrderedModule 𝕜 β
s : Set 𝕜
f : 𝕜 → β
x y z : 𝕜
hf : ConvexOn 𝕜 s f
hx : x ∈ s
hy : y ∈ s
hz : z ∈ Set.Icc x y
⊢ f z ≤ max (f x) (f y)
have hz₁ : z ∈ [x -[𝕜] y]
Tactic: rw [← segment_eq_Icc (hz.1.trans hz.2)] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
⊢ BddAbove (f '' (convexHull 𝕜 : (a : Set E) → Set E) s)
have refine : b ∈ upperBounds (f '' (convexHull 𝕜 : (a : Set E) → Set E) s)
Tactic: refine ⟨b, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Jensen (goal)
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 𝕜 β
f : E → β
s t : Set E
hst : s ⊆ t
hf : ConvexOn 𝕜 t f
b : β
hb : b ∈ upperBounds (f '' s)
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ f x ≤ b
have obtain : ∀ (y : E) (hy : y ∈ s) (hxy : f x ≤ f y), f x ≤ b
Tactic: obtain ⟨y, hy, hxy⟩ := hf.exists_ge_of_mem_convexHull hst hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s₁ s₂ t : Set E
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
have simp_rw : Eq.{u_3 + 1} (α := Set E) (⋃ x ∈ s₁ ∪ s₂, ⋃ y ∈ t, segment 𝕜 x y)
  ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
Tactic: simp_rw [convexJoin, mem_union, iUnion_or, iUnion_union_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s₁ s₂ t : Set E
simp_rw :
  Eq.{u_3 + 1} (α := Set E) (⋃ x ∈ s₁ ∪ s₂, ⋃ y ∈ t, segment 𝕜 x y)
    ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
have simp_rw₁ : Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (_ : x ∈ s₁ ∨ x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y)
  ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
Tactic: simp_rw [convexJoin, mem_union, iUnion_or, iUnion_union_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s₁ s₂ t : Set E
simp_rw :
  Eq.{u_3 + 1} (α := Set E) (⋃ x ∈ s₁ ∪ s₂, ⋃ y ∈ t, segment 𝕜 x y)
    ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
simp_rw₁ :
  Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (_ : x ∈ s₁ ∨ x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y)
    ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
⊢ convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
have simp_rw₂ : Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), (⋃ (_ : x ∈ s₁), ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ (_ : x ∈ s₂), ⋃ y ∈ t, segment 𝕜 x y)
  ((⋃ x ∈ s₁, ⋃ y ∈ t, segment 𝕜 x y) ∪ ⋃ x ∈ s₂, ⋃ y ∈ t, segment 𝕜 x y)
Tactic: simp_rw [convexJoin, mem_union, iUnion_or, iUnion_union_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s t₁ t₂ : Set E
⊢ convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂
have simp_rw : convexJoin 𝕜 (t₁ ∪ t₂) s = convexJoin 𝕜 t₁ s ∪ convexJoin 𝕜 t₂ s
Tactic: simp_rw [convexJoin_comm s, convexJoin_union_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : ι → Set E
t : Set E
⊢ convexJoin 𝕜 (⋃ (i : ι), s i) t = ⋃ (i : ι), convexJoin 𝕜 (s i) t
have simp_rw : Eq.{u_3 + 1} (α := Set E) (⋃ (x : E), ⋃ (i : ι), ⋃ (_ : x ∈ s i), ⋃ y ∈ t, segment 𝕜 x y)
  (⋃ (i : ι), ⋃ x ∈ s i, ⋃ y ∈ t, segment 𝕜 x y)
Tactic: simp_rw [convexJoin, mem_iUnion, iUnion_exists]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
t : ι → Set E
⊢ convexJoin 𝕜 s (⋃ (i : ι), t i) = ⋃ (i : ι), convexJoin 𝕜 s (t i)
have simp_rw : convexJoin 𝕜 (⋃ (i : ι), t i) s = ⋃ (i : ι), convexJoin 𝕜 (t i) s
Tactic: simp_rw [convexJoin_comm s, convexJoin_iUnion_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)
have simp_rw : ∀ (x : E),
  (∃ (a : E), (∃ a_1 ∈ s, ∃ b ∈ t, a ∈ segment 𝕜 a_1 b) ∧ ∃ b ∈ u, x ∈ segment 𝕜 a b) →
    ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ x ∈ segment 𝕜 a b
Tactic: simp_rw [subset_def, mem_convexJoin]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
⊢ ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
have inl : ∀ (hb₂ : LE.le.{u_2} (α := 𝕜) 0 0) (hab₂ : a₂ + 0 = 1),
  ∃ a ∈ s,
    ∃ (b : E),
      (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧
        a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z ∈ segment 𝕜 a b
Tactic: obtain rfl | hb₂ := hb₂.eq_or_lt
Cleared hypotheses: b₂, hb₂, hab₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
inl :
  ∀ (hb₂ : LE.le.{u_2} (α := 𝕜) 0 0) (hab₂ : a₂ + 0 = 1),
    ∃ a ∈ s,
      ∃ (b : E),
        (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧
          a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z ∈ segment 𝕜 a b
⊢ ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
have inr : ∀ (hb₂ : 0 < b₂),
  ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
Tactic: obtain rfl | hb₂ := hb₂.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : LE.le.{u_2} (α := 𝕜) 0 0
hab₂ : a₂ + 0 = 1
⊢ ∃ a ∈ s,
    ∃ (b : E),
      (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧
        a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z ∈ segment 𝕜 a b
have inl : a₁ • x + b₁ • y = a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z
Tactic: refine ⟨x, hx, y, ⟨y, hy, z, hz, left_mem_segment 𝕜 _ _⟩, a₁, b₁, ha₁, hb₁, hab₁, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : LE.le.{u_2} (α := 𝕜) 0 0
hab₂ : a₂ + 0 = 1
⊢ a₁ • x + b₁ • y = a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z
have a : a₁ • x + b₁ • y + (a₂ + 0) • (a₁ • x + b₁ • y) -
    (a₂ • (a₁ • x + b₁ • y) + HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 0 z +
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 1 (a₁ • x + b₁ • y)) =
  0
Tactic: linear_combination (norm := module) -hab₂ • (a₁ • x + b₁ • y)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
have inr : a₂ * a₁ + (a₂ * b₁ + b₂) = 1
Tactic: refine
    ⟨x, hx, (a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z,
      ⟨y, hy, z, hz, _, _, by positivity, by positivity, by field, rfl⟩,
      a₂ * a₁, a₂ * b₁ + b₂, by positivity, by positivity, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Join (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂_1 : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
inr : a₂ * a₁ + (a₂ * b₁ + b₂) = 1
⊢ ∃ a ∈ s, ∃ (b : E), (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b
have inr₁ : (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
  a₂ • (a₁ • x + b₁ • y) + b₂ • z
Tactic: refine
    ⟨x, hx, (a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z,
      ⟨y, hy, z, hz, _, _, by positivity, by positivity, by field, rfl⟩,
      a₂ * a₁, a₂ * b₁ + b₂, by positivity, by positivity, ?_, ?_⟩