awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ convexCombination (StdSimplex.map convexCombination f) = convexCombination f.join
have simp : 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 =
  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
Tactic: simp only [convexCombination, hL, hR]
-- 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
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
⊢ 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 =
    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
have e_a : Eq.{u_2 + 1} (α := V)
  (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
      (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
    V)
  ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V)
Tactic: congr 1
-- 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
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
⊢ Eq.{u_2 + 1} (α := V)
    (((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b : (a : P → R) → V)
        (⇑(StdSimplex.map convexCombination f).weights : (a : P) → R) :
      V)
    ((f.join.weights.support.weightedVSubOfPoint id b : (a : P → R) → V) (⇑f.join.weights : (a : P) → R) : V)
have e_a : 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: simp only [Finset.weightedVSubOfPoint_apply, StdSimplex.map, StdSimplex.join, id]
-- 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
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
⊢ 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))
have 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))
Tactic: change (Finsupp.mapDomain convexCombination f.weights).sum (fun x w => w • (x -ᵥ b)) = _
-- 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
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
⊢ 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))
have 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))
Tactic: rw [Finsupp.sum_mapDomain_index (fun _ => by simp) (fun _ _ _ => by simp [add_smul])]
-- 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
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
⊢ 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))
have 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))
Tactic: simp only [Finsupp.sum, convexCombination]
-- 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
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 ∈ 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)
have s : f.weights.support
Tactic: congr
-- 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
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
| ∑ 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)
have 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)
Tactic: congr
-- 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
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
| 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)
have 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)
Tactic: ext d
-- 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
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
| 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)
have 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))
Tactic: rw [d.weights.support.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
        _ _ d.total b, vadd_vsub, Finset.weightedVSubOfPoint_apply]
-- 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
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
| 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))
have 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))
Tactic: simp only [id]
-- 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
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 ∈ 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)
have 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))
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]
-- 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
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
⊢ 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))
have 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))
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]