-- 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)
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)
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) (ht : t = cons j (cons k u hk) ⋯), 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) (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)
obtain₇ :
  ∀ (j k : ι) (hjk : p j ≠ p k) (u : Finset ι) (hj : j ∉ u) (hk : k ∉ u) (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_1 : j ∈ cons j (cons k u hk) ⋯) (hk_1 : 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)
obtain₈ :
  ∀ (j k : ι) (hjk : p j ≠ p k) (u : Finset ι) (hj : j ∉ u) (hk : k ∉ u) (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_1 : j ∈ cons j (cons k u hk) ⋯) (hk_1 : k ∈ cons j (cons k u hk) ⋯)
    (this : k ∈ (cons j (cons k u hk) ⋯).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))
obtain₉ :
  ∀ (j k : ι) (hjk : p j ≠ p k) (u : Finset ι) (hj : j ∉ u) (hk : k ∉ u) (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_1 : j ∈ cons j (cons k u hk) ⋯) (hk_1 : k ∈ cons j (cons k u hk) ⋯)
    (this : k ∈ (cons j (cons k u hk) ⋯).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))
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
have obtain₁₀ : ∀ (j k : ι) (hjk : p j ≠ p k) (u : Finset ι) (hj : j ∉ u) (hk : k ∉ u) (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_1 : j ∈ cons j (cons k u hk) sorry) (hk_1 : k ∈ cons j (cons k u hk) sorry) (this : k ∈ (cons j (cons k u hk) sorry).erase j)
  (this : 0 < w j) (this : 0 < 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))
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: t, h₀, h₁, hmem, hp