-- Module: Mathlib.Analysis.Convex.StoneSeparation
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
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)
let :
  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) =
      (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))
let₁ let₂ :
  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 + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y))) =
      HSMul.hSMul (β := E) (az * av + bz * au)⁻¹ (∑ i : Fin 3, w i • z i)
e_a :
  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)),
    (au * av) • (az • x + bz • y) =
      List.foldr (fun (x1 x2 : E) ↦ x1 + x2) 0
        (List.map (fun (i : Fin 3) ↦ w i • z i)
          ((fun (x1 : Fin 3) (x2 : List (Fin 3)) ↦ (fun (i : Fin 3) ↦ i) x1 :: x2) ⟨2, ⋯⟩ []))
⊢ 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))

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]

Premises used: HMul.hMul, HAdd.hAdd, Finset.centerMass, HSMul.hSMul