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
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) ⋯
subst :
  ∀ (h₀ : ∀ i ∈ cons j (cons k u hk) ⋯, 0 < w i) (h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ cons j (cons k u hk) ⋯, w i) 1)
    (hmem : ∀ i ∈ cons j (cons k u hk) ⋯, p i ∈ s) (hj_2 : j ∈ cons j (cons k u hk) ⋯)
    (hk_2 : k ∈ cons j (cons k u hk) ⋯) (this : k ∈ (cons j (cons k u hk) ⋯).erase j),
    f (∑ i ∈ cons j (cons k u hk) ⋯, w i • p i) < ∑ i ∈ cons j (cons k u hk) ⋯, w i • f (p i)
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
subst ht
-- 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 → β
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
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))
⊢ 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)

Tactic:
simp only [sum_cons]

Premises used: Finset.sum_cons
-- 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 → β
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
⊢ j ∈ cons j (cons k u hk_1) ⋯

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 → β
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
⊢ 0 < w j

Tactic:
have := h₀ j <| by 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 → β
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
⊢ k ∈ cons j (cons k u hk_1) ⋯

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 → β
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
⊢ 0 < w k

Tactic:
have := h₀ k <| by 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 → β
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
⊢ w j / c + w k / c = 1

Tactic:
simp [field, c]
-- 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 → β
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
⊢ w j / c + w k / c = 1

Tactic:
have hc : w j / c + w k / c = 1 := by simp [field, c]
-- 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 → β
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
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
⊢ 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)

Tactic:
congrm f ?_
-- 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 → β
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)
match_scalars₂ : Eq.{u_1 + 1} (α := 𝕜) 1 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

Tactic:
match_scalars
-- 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 → β
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 * 1 = c * (w j / c * 1)

Tactic:
simp [field, c]
-- 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 → β
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 k * 1 = c * (w k / c * 1)

Tactic:
simp [field, c]
-- 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 → β
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
⊢ Eq.{u_1 + 1} (α := 𝕜) 1 1

Tactic:
simp [field, c]
-- 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 → β
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
i : ι
hi : i ∈ u
⊢ i ∈ cons j (cons k u hk_1) ⋯

Tactic:
simp [hi]
-- 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 → β
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 + ∑ i ∈ u, w i = 1

Tactic:
simpa [-cons_eq_insert, ← add_assoc] using h₁

Premises used: add_assoc, Finset.cons_eq_insert
-- 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 → β
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
⊢ 0 ≤ c

Tactic:
positivity
-- 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 → β
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
⊢ j ∈ cons j (cons k u hk_1) ⋯

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 → β
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
⊢ k ∈ cons j (cons k u hk_1) ⋯

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 → β
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
refine_2 : 0 ≤ w k / c
⊢ (w j / c) • p j + (w k / c) • p k ∈ s

Tactic:
refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc

Premises used: And.left
-- 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 → β
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
⊢ 0 ≤ w j / c

Tactic:
positivity
-- 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 → β
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
⊢ 0 ≤ w k / c

Tactic:
positivity
-- 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 → β
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 : f ((w j / c) • p j + (w k / c) • p k) < (w j / c) • f (p j) + (w k / c) • f (p k)
⊢ 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)

Tactic:
gcongr
-- 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 → β
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
bc₁ : 0 < w k / c
⊢ f ((w j / c) • p j + (w k / c) • p k) < (w j / c) • f (p j) + (w k / c) • f (p k)

Tactic:
refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc

Premises used: And.right
-- 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 → β
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
⊢ 0 < w j / c

Tactic:
positivity
-- 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 → β
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
⊢ 0 < w k / c

Tactic:
positivity
-- 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 → β
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 : c * (w j / c * 1) = w j * 1
match_scalars₁ : c * (w k / c * 1) = w k * 1
match_scalars₂ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) =
    w j • f (p j) + w k • f (p k) + ∑ x ∈ u, w x • f (p x)

Tactic:
match_scalars