-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
Use :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y
Use₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    1
Use₂ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y
Use₃ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    1
Use₄ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y
Use₅ Use₆ :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
    1
Use₇ Use₈ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y
e_a :
  ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
        (a : P → R) → V)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y)
⊢ (Finset.affineCombination R (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support id :
        (a : P → R) → P)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y) +ᵥ y
have e_a₁ : ∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R) (id i -ᵥ y) =
  s • (x -ᵥ y)
Tactic: classical
  -- Use weighted subtraction with base point y
  rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]
  swap
  · -- Prove sum of weights equals 1
    trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r
    · apply Finset.sum_congr rfl
      intro i _
      simp only [Finsupp.coe_add, Pi.add_apply]
    · rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]
  -- Now simplify the weighted subtraction
  congr 1
  rw [Finset.weightedVSubOfPoint_apply]
  simp only [id]
  -- Convert to Finsupp.sum
  change (Finsupp.single x s + Finsupp.single y t).sum (fun p w => w • (p -ᵥ y)) = _
  rw [Finsupp.sum_add_index (by simp) (fun _ a b => by simp [add_smul]),
    Finsupp.sum_single_index (by simp), Finsupp.sum_single_index (by simp)]
  simp [vsub_self]