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
h : P → R → V := fun (x : P) (w : R) ↦ w • (x -ᵥ b)
h_rhs :
  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
⊢ 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))

Tactic:
simp only [Finsupp.sum] at h_rhs ⊢

Premises used: Finsupp.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)
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))
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 ∈ 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))
⊢ 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))

Tactic:
rw [h_rhs]
-- 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))
e_a :
  Eq (α := StdSimplex R P → V)
    (fun (x : StdSimplex R P) ↦
      ∑ 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))
    fun (x : StdSimplex R P) ↦
    ∑ 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)
⊢ 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 ∈ 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))

Tactic:
congr 1
-- 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))
e_a :
  ∀ (d : StdSimplex R P),
    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))
      (∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support,
        h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) a))
⊢ Eq (α := StdSimplex R P → V)
    (fun (x : StdSimplex R P) ↦
      ∑ 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))
    fun (x : StdSimplex R P) ↦
    ∑ 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)

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
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
e_a :
  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))
    (∑ a ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support,
      h a ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) a))

Tactic:
simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]

Premises used: Finsupp.coe_smul, smul_eq_mul, Pi.smul_apply
-- 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
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)))

Tactic:
simp [hd]
-- 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
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)))

Tactic:
Finset.sum_congr ?_ (fun _ _ => rfl)

Premises used: Finset.sum_congr, rfl
-- 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
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
neg : d.weights.support = (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support
⊢ 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:
refine Finset.sum_congr ?_ (fun _ _ => rfl)

Premises used: Finset.sum_congr, rfl
-- 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
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
neg :
  ∀ (p : P),
    p ∈ d.weights.support ↔ p ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support
⊢ d.weights.support = (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support

Tactic:
ext p
-- 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
hd : ¬Eq.{u_1 + 1} (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) (0 : R)
p : P
neg :
  ¬Eq.{u_1 + 1} (α := R) ((d.weights : (a : P) → R) p : R) (0 : R) ↔
    ¬Eq.{u_1 + 1} (α := R)
        ((HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights : (a : P) → R) p : R) (0 : R)
⊢ p ∈ d.weights.support ↔ p ∈ (HSMul.hSMul (α := R) ((f.weights : (a : StdSimplex R P) → R) d : R) d.weights).support

Tactic:
simp only [Finsupp.mem_support_iff, ne_eq]

Premises used: Finsupp.mem_support_iff, ne_eq