-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
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
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id : (a : P → R) → P)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
          (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
        V)
      b
hR :
  (Finset.affineCombination R f.join.weights.support id : (a : P → R) → P) (⇑f.join.weights : (a : P) → R) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V) b
h : P → R → V := fun (x : P) (w : R) ↦ w • (x -ᵥ b)
h_rhs :
  Eq.{u_2 + 1} (α := V)
    (∑
      a ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights),
      h a
        ((∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights :
            (a : P) → R)
          a))
    (∑ x ∈ f.weights.support,
      ∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights).support,
        h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights : (a : P) → R) a))
d : StdSimplex R P
pos :
  ∀ (hd : Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)),
    Eq.{u_2 + 1} (α := V)
      (∑ x ∈ d.weights.support,
        HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R) ((d.weights : (a : P) → R) x : R) •
          (x -ᵥ b))
      (∑ x ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support,
        h x
          (HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R)
            ((d.weights : (a : P) → R) x : R)))
neg :
  ∀ (hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)),
    Eq.{u_2 + 1} (α := V)
      (∑ x ∈ d.weights.support,
        HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R) ((d.weights : (a : P) → R) x : R) •
          (x -ᵥ b))
      (∑ x ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support,
        h x
          (HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R)
            ((d.weights : (a : P) → R) x : R)))
⊢ Eq.{u_2 + 1} (α := V)
    (∑ x ∈ d.weights.support,
      HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R) ((d.weights : (a : P) → R) x : R) •
        (x -ᵥ b))
    (∑ x ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support,
      h x
        (HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) d : R) ((d.weights : (a : P) → R) x : R)))

Tactic:
by_cases hd : f.weights d = 0

Premises used: Convexity.StdSimplex.weights, DFunLike.coe