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 → β
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 * (w j / c * 1) = w j * 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
⊢ c * (w k / c * 1) = w k * 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 j • f (p j) + w k • 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:
abel_nf
-- 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
calc :
  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)
calc₁ :
  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)
calc₂ :
  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)
calc₃ :
  w j • f (p j) + w k • 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))
⊢ 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:
calc 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) := by
      congrm f ?_
      match_scalars <;> simp [field, c]
    _ ≤ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) :=
      -- apply the usual Jensen's inequality w.r.t. the weighted average of the two distinguished
      -- points and all the other points
        hf.convexOn.map_add_sum_le (fun i hi ↦ (h₀ _ <| by simp [hi]).le)
          (by simpa [-cons_eq_insert, ← add_assoc] using h₁)
          (forall_of_forall_cons <| forall_of_forall_cons hmem) (by positivity) <| by
           refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc <;> positivity
    _ < c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) := by
      -- then apply the definition of strict convexity for the two distinguished points
      gcongr; refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc <;> positivity
    _ = (w j • f (p j) + w k • f (p k)) + ∑ x ∈ u, w x • f (p x) := by
      match_scalars <;> simp [field, c]
    _ = w j • f (p j) + (w k • f (p k) + ∑ x ∈ u, w x • f (p x)) := by abel_nf

Premises used: HDiv.hDiv, LT.lt.le, Finset.forall_of_forall_cons, HAdd.hAdd, HSMul.hSMul, StrictConvexOn.convexOn, Finset.sum, ConvexOn.map_add_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 : 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
hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ ∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i)

Tactic:
hf.dual.map_sum_lt h₀ h₁ hmem hp

Premises used: StrictConvexOn.map_sum_lt, OrderDual, StrictConcaveOn.dual
-- 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
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
by_contra! : ∀ (this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k), False
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k

Tactic:
by_contra!
-- 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
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False

Tactic:
h_eq.not_gt <| hf.map_sum_lt h₀ h₁ hmem this

Premises used: StrictConvexOn.map_sum_lt, LE.le.not_gt
-- 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
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False

Tactic:
exact h_eq.not_gt <| hf.map_sum_lt h₀ h₁ hmem this

Premises used: StrictConvexOn.map_sum_lt, LE.le.not_gt
-- 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
h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
by_contra! : ∀ (this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k), False
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k

Tactic:
by_contra!
-- 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
h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False

Tactic:
h_eq.not_gt <| hf.lt_map_sum h₀ h₁ hmem this

Premises used: StrictConcaveOn.lt_map_sum, LE.le.not_gt
-- 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
h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k
⊢ False

Tactic:
exact h_eq.not_gt <| hf.lt_map_sum h₀ h₁ hmem this

Premises used: StrictConcaveOn.lt_map_sum, LE.le.not_gt
-- 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
mp : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
mpr : (∀ j ∈ t, p j = ∑ i ∈ t, w i • p i) → f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
constructor
-- 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
mp :
  ∀ (h₀ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 < w i) (h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ ∅, w i) 1)
    (hmem : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p i ∈ s),
    f (∑ i ∈ ∅, w i • p i) = ∑ i ∈ ∅, w i • f (p i) →
      ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → p j = ∑ i ∈ ∅, w i • p i
mp₁ : ∀ (i₀ : ι) (hi₀ : i₀ ∈ t), f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i

Tactic:
obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- 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
h₀ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 < w i
h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ ∅, w i) 1
hmem : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → p i ∈ s
⊢ f (∑ i ∈ ∅, w i • p i) = ∑ i ∈ ∅, w i • f (p i) →
    ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → p j = ∑ i ∈ ∅, w i • p i

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
i₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
⊢ p j = p i₀

Tactic:
apply hf.eq_of_le_map_sum h₀ h₁ hmem h_eq.ge hj hi₀

Premises used: Eq.ge, StrictConvexOn.eq_of_le_map_sum
-- 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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
⊢ ∀ j ∈ t, p j = p i₀

Tactic:
have H : ∀ j ∈ t, p j = p i₀ := by
      intro j hj
      apply hf.eq_of_le_map_sum h₀ h₁ hmem h_eq.ge hj 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 → β
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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
rw rw₁ : p i₀ = p i₀
⊢ p i = p i₀

Tactic:
rw [H _ 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 → β
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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
⊢ p i₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀)

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
i₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
rw rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∑ j ∈ t, w j) (p i₀)

Tactic:
rw [h₁]
-- 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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
rw rw₁ : Eq.{u_2 + 1} (α := E) (∑ i ∈ t, w i • p i₀) (∑ j ∈ t, w j • p i₀)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∑ j ∈ t, w j) (p i₀) = ∑ j ∈ t, w j • p i₀

Tactic:
rw [sum_smul]

Premises used: Finset.sum_smul
-- 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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
a : ∀ (j : ι) (hj : j ∈ t), p i₀ = p j
⊢ Eq.{u_2 + 1} (α := E) (∑ j ∈ t, w j • p i₀) (∑ j ∈ t, w j • p j)

Tactic:
congr! 2 with j hj
-- 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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
j : ι
hj : j ∈ t
a a₁ : p j = p j
⊢ p i₀ = p j

Tactic:
rw [← H _ hj]
-- 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₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
H : ∀ j ∈ t, p j = p i₀
calc : p i = p i₀
calc₁ : p i₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀)
calc₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∑ j ∈ t, w j) (p i₀)
calc₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∑ j ∈ t, w j) (p i₀) = ∑ j ∈ t, w j • p i₀
calc₄ : Eq.{u_2 + 1} (α := E) (∑ j ∈ t, w j • p i₀) (∑ j ∈ t, w j • p j)
⊢ p i = ∑ i ∈ t, w i • p i

Tactic:
calc p i = p i₀ := by rw [H _ hi]
      _ = (1 : 𝕜) • p i₀ := by simp
      _ = (∑ j ∈ t, w j) • p i₀ := by rw [h₁]
      _ = ∑ j ∈ t, (w j • p i₀) := by rw [sum_smul]
      _ = ∑ j ∈ t, (w j • p j) := by congr! 2 with j hj; rw [← H _ hj]

Premises used: OfNat.ofNat, Finset.sum
-- 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
h : ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
j : ι
hj : j ∈ t
⊢ w j • f (p j) = w j • f (∑ i ∈ t, w i • p i)

Tactic:
simp [h j hj]
-- 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
h : ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
⊢ ∀ j ∈ t, w j • f (p j) = w j • f (∑ i ∈ t, w i • p i)

Tactic:
have H : ∀ j ∈ t, w j • f (p j) = w j • f (∑ i ∈ t, w i • p i) := by
      intro j hj
      simp [h j hj]
-- 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
h : ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
H : ∀ j ∈ t, w j • f (p j) = w j • f (∑ i ∈ t, w i • p i)
mpr : f (∑ i ∈ t, w i • p i) = ∑ x ∈ t, w x • f (∑ i ∈ t, w i • p i)
mpr₁ : f (∑ i ∈ t, w i • p i) = HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (∑ i ∈ t, w i) (f (∑ i ∈ t, w i • p i))
mpr₂ : f (∑ i ∈ t, w i • p i) = HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 (f (∑ i ∈ t, w i • p i))
mpr₃ mpr₄ : f (∑ i ∈ t, w i • p i) = f (∑ i ∈ t, w i • p i)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)

Tactic:
rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]

Premises used: Finset.sum_smul, one_smul, Finset.sum_congr, rfl
-- 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, p j = ∑ i ∈ t, w i • p i

Tactic:
simpa using hf.neg.map_sum_eq_iff h₀ h₁ hmem

Premises used: StrictConvexOn.map_sum_eq_iff, StrictConcaveOn.neg
-- 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 : ι
h : i ∈ t
⊢ w i • p i ≠ 0 → w i ≠ 0

Tactic:
simp_all