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
⊢ 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))
have 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))
Tactic: simp_rw [Finset.smul_sum, smul_smul]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (hypothesis)
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)
⊢ 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))
have 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
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
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (hypothesis)
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)
    (∑ 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))
have 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))
Tactic: simp only [Finsupp.sum] at h_rhs ⊢
Cleared hypotheses: h_rhs
-- 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
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))
⊢ 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))
have 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))
Tactic: rw [h_rhs]
-- 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
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))
⊢ 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))
have 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)
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
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))
⊢ 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)
have 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))
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
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
⊢ 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))
have 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)))
Tactic: simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]
-- 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
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
⊢ 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)))
have 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)))
Tactic: by_cases hd : f.weights d = 0
-- 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
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)))
⊢ 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)))
have 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)))
Tactic: by_cases hd : f.weights d = 0