-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
inr inr₁ inr₂ inr₃ :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E)
    ((az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q))
inr₄ :
  let w := ![az * av * bu, bz * au * bv, au * av];
  ∀ (hw₀ : ∀ (i : Fin 3), 0 ≤ w i),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E)
      ((az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q))
inr₅ :
  let w := ![az * av * bu, bz * au * bv, au * av];
  ∀ (hw₀ : ∀ (i : Fin 3), 0 ≤ w i) (hw : ∑ i : Fin 3, w i = az * av + bz * au),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E)
      ((az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q))
inr₆ :
  let w := ![az * av * bu, bz * au * bv, au * av];
  let z := ![p, q, az • x + bz • y];
  ∀ (hw₀ : ∀ (i : Fin 3), 0 ≤ w i) (hw : ∑ i : Fin 3, w i = az * av + bz * au)
    (hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E)
      ((az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q))
h :
  let w := ![az * av * bu, bz * au * bv, au * av];
  let z := ![p, q, az • x + bz • y];
  ∀ (hw₀ : ∀ (i : Fin 3), 0 ≤ w i) (hw : ∑ i : Fin 3, w i = az * av + bz * au)
    (hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)),
    (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
      Finset.centerMass Finset.univ w z
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E)
    ((az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q))
have h₁ : let w := ![az * av * bu, bz * au * bv, au * av];
let z := ![p, q, az • x + bz • y];
∀ (hw₀ : ∀ (i : Fin 3), 0 ≤ w i) (hw : ∑ i : Fin 3, w i = az * av + bz * au)
  (hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)),
  (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    HSMul.hSMul (β := E) (az * av + bz * au)⁻¹ (∑ i : Fin 3, w i • z i)
Tactic: classical
    let w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
    let z : Fin 3 → E := ![p, q, az • x + bz • y]
    have hw₀ : ∀ i, 0 ≤ w i := by
      rintro i
      fin_cases i
      · exact mul_nonneg (mul_nonneg haz hav) hbu
      · exact mul_nonneg (mul_nonneg hbz hau) hbv
      · exact mul_nonneg hau hav
    have hw : ∑ i, w i = az * av + bz * au := by
      trans az * av * bu + (bz * au * bv + au * av)
      · simp [w, Fin.sum_univ_succ]
      linear_combination (au * bv - 1 * au) * habz + (-(1 * az * au) + au) * habv + az * av * habu
    have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp [z]
    convert!
      (Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i)
          (by rwa [hw]) fun i _ => hz i :
        Finset.univ.centerMass w z ∈ _)
    rw [Finset.centerMass, hw]
    trans (az * av + bz * au)⁻¹ •
      ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))
    · module
    congr 3
    simp [w, z]