awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e_a :
  Eq.{u_2 + 1} (α := V) ((Finsupp.mapDomain convexCombination f.weights).sum fun (x : P) (w : R) ↦ w • (x -ᵥ b))
    (∑ x ∈ Finsupp.support.{u_3, u_1} (M := R) (f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights : (a : P) → R) x : R) (x -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V)
    (∑ x ∈ (Finsupp.mapDomain convexCombination f.weights).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Finsupp.mapDomain convexCombination f.weights : (a : P) → R) x : R)
        (x -ᵥ b))
    (∑ x ∈ Finsupp.support.{u_3, u_1} (M := R) (f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights : (a : P) → R) x : R) (x -ᵥ b))

Tactic:
change (Finsupp.mapDomain convexCombination f.weights).sum (fun x w => w • (x -ᵥ b)) = _

Premises used: Finsupp.mapDomain, Finsupp.sum, VSub.vsub, Convexity.StdSimplex.weights, AddTorsor.convexCombination, HSMul.hSMul
-- 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
x : P
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x -ᵥ b) = 0

Tactic:
simp
-- 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
x : P
x_1 x_2 : R
⊢ (x_1 + x_2) • (x -ᵥ b) = x_1 • (x -ᵥ b) + x_2 • (x -ᵥ b)

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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
e_a :
  Eq.{u_2 + 1} (α := V) (f.weights.sum fun (a : StdSimplex R P) (m : R) ↦ m • (convexCombination a -ᵥ b))
    (∑ x ∈ Finsupp.support.{u_3, u_1} (M := R) (f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights : (a : P) → R) x : R) (x -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V) ((Finsupp.mapDomain convexCombination f.weights).sum fun (x : P) (w : R) ↦ w • (x -ᵥ b))
    (∑ x ∈ Finsupp.support.{u_3, u_1} (M := R) (f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights : (a : P) → R) x : R) (x -ᵥ b))

Tactic:
rw [Finsupp.sum_mapDomain_index (fun _ => by simp) (fun _ _ _ => by simp [add_smul])]

Premises used: Finsupp.sum_mapDomain_index
-- 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
e_a :
  Eq.{u_2 + 1} (α := V)
    (∑ x ∈ f.weights.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R)
        ((Finset.affineCombination R x.weights.support id : (a : P → R) → P) (⇑x.weights : (a : P) → R) -ᵥ b))
    (∑
      x ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights :
              (a : P) → R)
            x :
          R)
        (x -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V) (f.weights.sum fun (a : StdSimplex R P) (m : R) ↦ m • (convexCombination a -ᵥ b))
    (∑ x ∈ Finsupp.support.{u_3, u_1} (M := R) (f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((f.weights.sum fun (d : StdSimplex R P) (r : R) ↦ r • d.weights : (a : P) → R) x : R) (x -ᵥ b))

Tactic:
simp only [Finsupp.sum, convexCombination]

Premises used: Finsupp.sum, AddTorsor.convexCombination
-- 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
s : f.weights.support
f₁ :
  fun (x : StdSimplex R P) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R)
      ((Finset.affineCombination R x.weights.support id : (a : P → R) → P) (⇑x.weights : (a : P) → R) -ᵥ b)
| ∑ x ∈ f.weights.support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R)
      ((Finset.affineCombination R x.weights.support id : (a : P → R) → P) (⇑x.weights : (a : P) → R) -ᵥ b)

Tactic:
congr
-- 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
| f.weights.support

Tactic:
· skip
-- 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
f₁ :
  ∀ (d : StdSimplex R P),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R)
      ((Finset.affineCombination R d.weights.support id : (a : P → R) → P) (⇑d.weights : (a : P) → R) -ᵥ b)
| fun (x : StdSimplex R P) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R)
      ((Finset.affineCombination R x.weights.support id : (a : P → R) → P) (⇑x.weights : (a : P) → R) -ᵥ b)

Tactic:
ext d
-- 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
d : StdSimplex R P
f₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((f.weights : (a : StdSimplex R P) → R) d : R)
    (∑ i ∈ d.weights.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : P) (r : R) ↦ r) i ((d.weights : (a : P) → R) i)) (id i -ᵥ b))
| HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R)
    ((Finset.affineCombination R d.weights.support id : (a : P → R) → P) (⇑d.weights : (a : P) → R) -ᵥ b)

Tactic:
rw [d.weights.support.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
        _ _ d.total b, vadd_vsub, Finset.weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply, Finsupp.support, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Convexity.StdSimplex.weights, Convexity.StdSimplex.total, vadd_vsub
-- 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
d : StdSimplex R P
f₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((f.weights : (a : StdSimplex R P) → R) d : R)
    (∑ x ∈ d.weights.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((d.weights : (a : P) → R) x : R) (x -ᵥ b))
| HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((f.weights : (a : StdSimplex R P) → R) d : R)
    (∑ i ∈ d.weights.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (x : P) (r : R) ↦ r) i ((d.weights : (a : P) → R) i)) (id i -ᵥ b))

Tactic:
simp only [id]

Premises used: id
-- 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
f₁ :
  ∀ (d : StdSimplex R P),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((f.weights : (a : StdSimplex R P) → R) d : R)
      (∑ x ∈ d.weights.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((d.weights : (a : P) → R) x : R) (x -ᵥ b))
| ∑ x ∈ f.weights.support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R)
      ((Finset.affineCombination R x.weights.support id : (a : P → R) → P) (⇑x.weights : (a : P) → R) -ᵥ b)

Tactic:
congr; · skip
    ext d
    rw [d.weights.support.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
        _ _ d.total b, vadd_vsub, Finset.weightedVSubOfPoint_apply]
    simp only [id]

Premises used: Finset.weightedVSubOfPoint_apply, id, vadd_vsub
-- 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
e_a :
  Eq.{u_2 + 1} (α := V)
    (∑ d ∈ f.weights.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((f.weights : (a : StdSimplex R P) → R) d : R)
        (∑ x ∈ d.weights.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((d.weights : (a : P) → R) x : R) (x -ᵥ b)))
    (∑
      x ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights :
              (a : P) → R)
            x :
          R)
        (x -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V)
    (∑ x ∈ f.weights.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R)
        ((Finset.affineCombination R x.weights.support id : (a : P → R) → P) (⇑x.weights : (a : P) → R) -ᵥ b))
    (∑
      x ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights :
              (a : P) → R)
            x :
          R)
        (x -ᵥ b))

Tactic:
conv_lhs =>
    congr; · skip
    ext d
    rw [d.weights.support.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
        _ _ d.total b, vadd_vsub, Finset.weightedVSubOfPoint_apply]
    simp only [id]

Premises used: Finset.weightedVSubOfPoint_apply, id, vadd_vsub
-- 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
e_a :
  Eq.{u_2 + 1} (α := V)
    (∑ x ∈ f.weights.support,
      ∑ x_1 ∈ x.weights.support,
        HMul.hMul (α := R) (β := R) ((f.weights : (a : StdSimplex R P) → R) x : R) ((x.weights : (a : P) → R) x_1 : R) •
          (x_1 -ᵥ b))
    (∑
      x ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights :
              (a : P) → R)
            x :
          R)
        (x -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V)
    (∑ d ∈ f.weights.support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V) ((f.weights : (a : StdSimplex R P) → R) d : R)
        (∑ x ∈ d.weights.support, HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((d.weights : (a : P) → R) x : R) (x -ᵥ b)))
    (∑
      x ∈
        Finsupp.support.{u_3, u_1} (M := R)
          (∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((∑ x ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) x : R) x.weights :
              (a : P) → R)
            x :
          R)
        (x -ᵥ b))

Tactic:
simp_rw [Finset.smul_sum, smul_smul]

Premises used: smul_smul, Finset.smul_sum
-- 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)
⊢ Finsupp.sum (∑ d ∈ f.weights.support, HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights)
      h =
    ∑ d ∈ f.weights.support, (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).sum h

Tactic:
have h_rhs : (∑ d ∈ f.weights.support, f.weights d • d.weights).sum h
      = ∑ d ∈ f.weights.support, (f.weights d • d.weights).sum h :=
    (Finsupp.sum_finsetSum_index (h := h) (fun _ => zero_smul _ _)
      (fun _ _ _ => add_smul _ _ _)).symm