awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
obtain₁ obtain₂ :
  ∀ (j : ι) (hj : j ∈ t) (k : ι) (hk : k ∈ t) (hjk : p j ≠ p k) (this : k ∈ t.erase j),
    f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
obtain₃ :
  ∀ (j : ι) (hj : j ∈ t) (k : ι) (hk : k ∈ t) (hjk : p j ≠ p k) (this : k ∈ t.erase j),
    let u := (t.erase j).erase k;
    ∀ (hj : j ∉ u), 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)
have obtain₄ : ∀ (j : ι) (hj : j ∈ t) (k : ι) (hk : k ∈ t) (hjk : p j ≠ p k) (this : k ∈ t.erase j),
  let u := (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)
Tactic: classical
  obtain ⟨j, hj, k, hk, hjk⟩ := hp
  -- We replace `t` by `t \ {j, k}`
  have : k ∈ t.erase j := mem_erase.2 ⟨ne_of_apply_ne _ hjk.symm, hk⟩
  let u := (t.erase j).erase k
  have hj : j ∉ u := by simp [u]
  have hk : k ∉ u := by simp [u]
  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›, *]
  clear_value u
  subst ht
  simp only [sum_cons]
  have := h₀ j <| by simp
  have := h₀ k <| by simp
  let c := w j + w k
  have hc : w j / c + w k / c = 1 := by simp [field, c]
  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
Cleared hypotheses: hp
-- 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
h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
have by_contra! : ∀ (this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k), False
Tactic: by_contra!
-- 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 : 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)
⊢ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
have by_contra! : ∀ (this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k), False
Tactic: by_contra!
-- 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
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
have 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
Tactic: constructor
-- 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
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
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
have 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)
Tactic: constructor
-- 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
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
have 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
Tactic: obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty
Cleared hypotheses: t, h₀, h₁, 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
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
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) → ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
have 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
Tactic: obtain rfl | ⟨i₀, hi₀⟩ := t.eq_empty_or_nonempty
-- 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
i₀ : ι
hi₀ : i₀ ∈ t
h_eq : f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
i : ι
hi : i ∈ t
⊢ p i = ∑ i ∈ t, w i • p i
have H : ∀ 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₀
-- 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
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 = p i₀
have rw : p i₀ = p i₀
Tactic: rw [H _ hi]
-- 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
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₀
⊢ 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₀)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀) = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (p i₀)
Tactic: rw [h₁]
-- 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
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₀
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∑ j ∈ t, w j) (p i₀) = ∑ j ∈ t, w j • p i₀
have rw : Eq.{u_2 + 1} (α := E) (∑ i ∈ t, w i • p i₀) (∑ j ∈ t, w j • p i₀)
Tactic: rw [sum_smul]
-- 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
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₀
⊢ Eq.{u_2 + 1} (α := E) (∑ j ∈ t, w j • p i₀) (∑ j ∈ t, w j • p j)
have a : ∀ (j : ι) (hj : j ∈ t), p i₀ = p j
Tactic: congr! 2 with j hj
-- 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
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
⊢ p i₀ = p j
have a : p j = p j
Tactic: rw [← H _ hj]
-- 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
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 = ∑ i ∈ t, w i • p i
have calc : p 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]
-- 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
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₀
⊢ p i = ∑ i ∈ t, w i • p i
have calc₁ : p i₀ = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (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]
-- 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
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₀)
⊢ p i = ∑ i ∈ t, w i • p i
have 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₀)
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]
-- 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
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₀)
⊢ p i = ∑ i ∈ t, w i • p i
have calc₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (∑ j ∈ t, w j) (p i₀) = ∑ j ∈ t, w j • 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]
-- 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
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₀
⊢ p i = ∑ i ∈ t, w i • p i
have calc₄ : Eq.{u_2 + 1} (α := E) (∑ j ∈ t, w j • p i₀) (∑ j ∈ t, w j • p j)
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]
-- 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
h : ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
have H : ∀ 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]
-- 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
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)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
have mpr : f (∑ i ∈ t, w i • p i) = ∑ x ∈ t, w x • f (∑ i ∈ t, w i • p i)
Tactic: rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]
-- 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
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)
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
have 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))
Tactic: rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]
-- 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
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))
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
have mpr₂ : f (∑ i ∈ t, w i • p i) = HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 (f (∑ i ∈ t, w i • p i))
Tactic: rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]
-- 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
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))
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i)
have mpr₃ : f (∑ i ∈ t, w i • p i) = f (∑ i ∈ t, w i • p i)
Tactic: rw [sum_congr rfl H, ← sum_smul, h₁, one_smul]
-- 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
⊢ 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 • p i ≠ 0 → w i ≠ 0
Tactic: have hw (i) (_ : i ∈ t) : w i • p i ≠ 0 → w i ≠ 0 := by simp_all