awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
Goal:
V : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (intrinsicInterior ℝ s).Nonempty → s.Nonempty
have simp_rw : intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅
Tactic: simp_rw [nonempty_iff_ne_empty]
-- 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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
have hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
Tactic: have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ { p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2 } := fun i hi =>
    ⟨hmem i hi, le_rfl⟩
-- 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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
have h : t.centerMass w p = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).1
Tactic: convert! (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2
-- 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 : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : LT.lt.{u_1} (α := 𝕜) 0 (∑ i ∈ t, w i)
hmem : ∀ i ∈ t, p i ∈ s
hmem' : ∀ i ∈ t, Membership.mem (γ := Set (E × β)) {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2} (p i, (f ∘ p) i)
h : t.centerMass w p = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).1
⊢ f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
have h₂ : t.centerMass w (f ∘ p) = (t.centerMass w fun (i : ι) ↦ (p i, (f ∘ p) i)).2
Tactic: convert! (hf.convex_epigraph.centerMass_mem h₀ h₁ hmem').2
-- 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
v : 𝕜
q : E
hf : ConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : v + ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
hv : 0 ≤ v
hq : q ∈ s
W : (j : Option ι) → 𝕜 := fun (j : Option ι) ↦ j.elim v w
P : (j : Option ι) → E := fun (j : Option ι) ↦ j.elim q p
⊢ f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)
have this : f (∑ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W j • P j) ≤
  ∑ j ∈ (insertNone : (a : Finset ι) → Finset (Option ι)) t, W j • f (P j)
Tactic: have : f (∑ j ∈ insertNone t, W j • P j) ≤ ∑ j ∈ insertNone t, W j • f (P j) :=
    hf.map_sum_le (forall_mem_insertNone.2 ⟨hv, h₀⟩) (by simpa using h₁)
      (forall_mem_insertNone.2 ⟨hq, hmem⟩)
-- 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
hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have obtain : ∀ (j : ι) (hj : j ∈ t) (k : ι) (hk : k ∈ t) (hjk : p j ≠ p k), f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
Tactic: obtain ⟨j, hj, k, hk, hjk⟩ := hp
Cleared hypotheses: 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 : 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
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have this : k ∈ t.erase j
Tactic: have : k ∈ t.erase j := mem_erase.2 ⟨ne_of_apply_ne _ hjk.symm, hk⟩
-- 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
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have hj₁ : j ∉ u
Tactic: have hj : j ∉ u := by simp [u]
-- 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
j : ι
hj_1 : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have hk₁ : k ∉ u
Tactic: have hk : k ∉ u := by simp [u]
-- 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
j : ι
hj_1 : j ∈ t
k : ι
hk_1 : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
hk : k ∉ u
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have ht : t = cons j (cons k u hk) sorry
Tactic: have ht :
      t = (u.cons k hk).cons j (mem_cons.not.2 <| not_or_intro (ne_of_apply_ne _ hjk) hj) := by
    simp [u, insert_erase this, insert_erase ‹j ∈ t›, *]
-- 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
j : ι
hj_1 : j ∈ t
k : ι
hk_1 : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
hk : k ∉ u
ht : t = cons j (cons k u hk) ⋯
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have clear_value : ∀ (u : Finset ι) (hj : j ∉ u) (hk : k ∉ u) (ht : t = cons j (cons k u hk) sorry),
  f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
Tactic: clear_value u
Cleared hypotheses: u, hj, hk, ht
-- 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
j : ι
hj_1 : j ∈ t
k : ι
hk_1 : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι
hj : j ∉ u
hk : k ∉ u
ht : t = cons j (cons k u hk) ⋯
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have subst : ∀ (h₀ : ∀ i ∈ cons j (cons k u hk) sorry, 0 < w i) (h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk) sorry, w i) 1)
  (hmem : ∀ i ∈ cons j (cons k u hk) sorry, p i ∈ s) (hj_2 : j ∈ cons j (cons k u hk) sorry) (hk_2 : k ∈ cons j (cons k u hk) sorry)
  (this : k ∈ (cons j (cons k u hk) sorry).erase j),
  f (∑ i ∈ cons j (cons k u hk) sorry, w i • p i) < ∑ i ∈ cons j (cons k u hk) sorry, w i • f (p i)
Tactic: subst ht
Cleared hypotheses: t, h₀, h₁, hmem, hj_1, hk_1, this, ht
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this : k ∈ (cons j (cons k u hk_1) ⋯).erase j
⊢ f (∑ i ∈ cons j (cons k u hk_1) ⋯, w i • p i) < ∑ i ∈ cons j (cons k u hk_1) ⋯, w i • f (p i)
have simp : f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))
Tactic: simp only [sum_cons]
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this : k ∈ (cons j (cons k u hk_1) ⋯).erase j
⊢ f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))
have this₁ : 0 < w j
Tactic: have := h₀ j <| by simp
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this : 0 < w j
⊢ f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))
have this₁ : 0 < w k
Tactic: have := h₀ k <| by simp
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
⊢ f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))
have hc : w j / c + w k / c = 1
Tactic: have hc : w j / c + w k / c = 1 := by simp [field, c]
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ f (w j • p j + (w k • p k + ∑ x ∈ u, w x • p x)) = f (c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x)
have congrm : w j • p j + (w k • p k + ∑ x ∈ u, w x • p x) = c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x
Tactic: congrm f ?_
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ w j • p j + (w k • p k + ∑ x ∈ u, w x • p x) = c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x
have match_scalars : w j * 1 = c * (w j / c * 1)
Tactic: match_scalars
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
match_scalars : w j * 1 = c * (w j / c * 1)
⊢ w j • p j + (w k • p k + ∑ x ∈ u, w x • p x) = c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x
have match_scalars₁ : w k * 1 = c * (w k / c * 1)
Tactic: match_scalars
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
match_scalars : w j * 1 = c * (w j / c * 1)
match_scalars₁ : w k * 1 = c * (w k / c * 1)
⊢ w j • p j + (w k • p k + ∑ x ∈ u, w x • p x) = c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x
have match_scalars₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: match_scalars
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ (w j / c) • p j + (w k / c) • p k ∈ s
have refine_1 : 0 ≤ w j / c
Tactic: refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
refine_1 : 0 ≤ w j / c
⊢ (w j / c) • p j + (w k / c) • p k ∈ s
have refine_2 : 0 ≤ w k / c
Tactic: refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) <
    c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x)
have bc : f ((w j / c) • p j + (w k / c) • p k) < (w j / c) • f (p j) + (w k / c) • f (p k)
Tactic: gcongr
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ f ((w j / c) • p j + (w k / c) • p k) < (w j / c) • f (p j) + (w k / c) • f (p k)
have bc : 0 < w j / c
Tactic: refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc
-- 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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj_1 : j ∉ u
hk_1 : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk_1) ⋯, 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk_1) ⋯, w i) 1
hmem : ∀ i ∈ cons j (cons k u hk_1) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk_1) ⋯
hk : k ∈ cons j (cons k u hk_1) ⋯
this_1 : k ∈ (cons j (cons k u hk_1) ⋯).erase j
this_2 : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
bc : 0 < w j / c
⊢ f ((w j / c) • p j + (w k / c) • p k) < (w j / c) • f (p j) + (w k / c) • f (p k)
have bc₁ : 0 < w k / c
Tactic: refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc