awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ b : P
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint (fun (i : ι) ↦ p₂) b : (a : ι → k) → V) w : V) =
    HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))
b₁ : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) =
    HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))
have rw₁ : HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b)) =
  HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))
Tactic: rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ b : P
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
have rw : HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint (fun (i : ι) ↦ p₁) b : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V) =
  HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
    ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
Tactic: rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ b : P
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint (fun (i : ι) ↦ p₁) b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
b₁ : P
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
have rw₁ : HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
    ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V) =
  HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
    ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
Tactic: rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ HAdd.hAdd (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
have simp_rw : HAdd.hAdd (α := V) (∑ i ∈ s \ s₂, w i • (p i -ᵥ b)) (∑ i ∈ s₂, w i • (p i -ᵥ b)) = ∑ i ∈ s, w i • (p i -ᵥ b)
Tactic: simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
have rw : HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    (-(s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
  (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
Tactic: rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
rw :
  HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      (-(s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
⊢ HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
have rw₁ : HAdd.hAdd (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
  (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
Tactic: rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
rw :
  HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      (-(s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
rw₁ :
  HAdd.hAdd (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
⊢ HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
have rw₂ : Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
  ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
Tactic: rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
⊢ Eq.{u_2 + 1} (α := V)
    (((Finset.subtype pred s).weightedVSubOfPoint (fun (i : Subtype pred) ↦ p (↑i : ι)) b : (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have rw : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b) : V)
  (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
rw :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b) : V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V)
    (((Finset.subtype pred s).weightedVSubOfPoint (fun (i : Subtype pred) ↦ p (↑i : ι)) b : (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b))
  (∑ i ∈ s with pred i, w i • (p i -ᵥ b))
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
rw :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b) : V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
rw₁ :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b))
    (∑ i ∈ s with pred i, w i • (p i -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V)
    (((Finset.subtype pred s).weightedVSubOfPoint (fun (i : Subtype pred) ↦ p (↑i : ι)) b : (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have rw₂ : Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b))
  (∑ x ∈ Finset.subtype pred s, w (↑x : ι) • (p (↑x : ι) -ᵥ b))
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
⊢ Eq.{u_2 + 1} (α := V) (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have rw : ∀ x ∈ s, w x • (p x -ᵥ b) ≠ 0 → pred x
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, sum_filter_of_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ pred i
have refine : w i ≠ 0
Tactic: refine h i hi ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
⊢ (s.weightedVSubOfPoint p b : (a : ι → k) → V) (c • w) =
    HSMul.hSMul (β := V) c ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have simp_rw : ∑ i ∈ s, (c • w) i • (p i -ᵥ b) = HSMul.hSMul (β := V) c (∑ i ∈ s, w i • (p i -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
simp_rw : ∑ i ∈ s, (c • w) i • (p i -ᵥ b) = HSMul.hSMul (β := V) c (∑ i ∈ s, w i • (p i -ᵥ b))
⊢ (s.weightedVSubOfPoint p b : (a : ι → k) → V) (c • w) =
    HSMul.hSMul (β := V) c ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, (c • w) i • (p i -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
simp_rw : ∑ i ∈ s, (c • w) i • (p i -ᵥ b) = HSMul.hSMul (β := V) c (∑ i ∈ s, w i • (p i -ᵥ b))
simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, (c • w) i • (p i -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
⊢ (s.weightedVSubOfPoint p b : (a : ι → k) → V) (c • w) =
    HSMul.hSMul (β := V) c ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have simp_rw₂ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (c • w x) • (p x -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
simp_rw : ∑ i ∈ s, (c • w) i • (p i -ᵥ b) = HSMul.hSMul (β := V) c (∑ i ∈ s, w i • (p i -ᵥ b))
simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, (c • w) i • (p i -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
simp_rw₂ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (c • w x) • (p x -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
⊢ (s.weightedVSubOfPoint p b : (a : ι → k) → V) (c • w) =
    HSMul.hSMul (β := V) c ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
have simp_rw₃ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (c • w x) • (p x -ᵥ b)) (∑ x ∈ s, (c * w x) • (p x -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ Eq.{u_2 + 1} (α := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : ι) ↦ p : (a : ι → k) → V) w : V) (0 : V)
have rw : Eq.{u_2 + 1} (α := V)
  ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice sorry) : (a : ι → k) → V) w : V)
  (0 : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  Eq.{u_2 + 1} (α := V)
    ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V) w :
      V)
    (0 : V)
⊢ Eq.{u_2 + 1} (α := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : ι) ↦ p : (a : ι → k) → V) w : V) (0 : V)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice sorry) = 0
Tactic: rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  Eq.{u_2 + 1} (α := V)
    ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V) w :
      V)
    (0 : V)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯) = 0
⊢ Eq.{u_2 + 1} (α := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : ι) ↦ p : (a : ι → k) → V) w : V) (0 : V)
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (p -ᵥ Classical.choice sorry) = 0
Tactic: rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  Eq.{u_2 + 1} (α := V)
    ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V) w :
      V)
    (0 : V)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯) = 0
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (p -ᵥ Classical.choice ⋯) = 0
⊢ Eq.{u_2 + 1} (α := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : ι) ↦ p : (a : ι → k) → V) w : V) (0 : V)
have rw₃ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
v : V
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub (v +ᵥ p) : (a : ι → k) → V) w : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw : Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint (v +ᵥ p) (Classical.choice sorry) : (a : ι → k) → V) w : V)
  ((s.weightedVSub p : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
v : V
rw :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint (v +ᵥ p) (Classical.choice ⋯) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub (v +ᵥ p) : (a : ι → k) → V) w : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw₁ : Eq.{u_2 + 1} (α := V)
  ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice sorry)) : (a : ι → k) → V) w : V)
  ((s.weightedVSub p : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
v : V
rw :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint (v +ᵥ p) (Classical.choice ⋯) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₁ :
  Eq.{u_2 + 1} (α := V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub (v +ᵥ p) : (a : ι → k) → V) w : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw₂ : Eq.{u_2 + 1} (α := V)
  ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice sorry)) : (a : ι → k) → V) w : V)
  ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice sorry)) : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
v : V
rw :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint (v +ᵥ p) (Classical.choice ⋯) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₁ :
  Eq.{u_2 + 1} (α := V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₂ :
  Eq.{u_2 + 1} (α := V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub (v +ᵥ p) : (a : ι → k) → V) w : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw₃ : P
Tactic: rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
G : Type u_6
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → V
a : G
⊢ (s.weightedVSub (a • p) : (a : ι → k) → V) w = HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw : (s.weightedVSubOfPoint (a • p) (Classical.choice sorry) : (a : ι → k) → V) w =
  HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
G : Type u_6
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → V
a : G
rw :
  (s.weightedVSubOfPoint (a • p) (Classical.choice ⋯) : (a : ι → k) → V) w =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
⊢ (s.weightedVSub (a • p) : (a : ι → k) → V) w = HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw₁ : HSMul.hSMul (β := V) a
    ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice sorry)) : (a : ι → k) → V) w : V) =
  HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
G : Type u_6
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → V
a : G
rw :
  (s.weightedVSubOfPoint (a • p) (Classical.choice ⋯) : (a : ι → k) → V) w =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₁ :
  HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V) =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
⊢ (s.weightedVSub (a • p) : (a : ι → k) → V) w = HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
have rw₂ : HSMul.hSMul (β := V) a
    ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice sorry)) : (a : ι → k) → V) w : V) =
  HSMul.hSMul (β := V) a
    ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice sorry)) : (a : ι → k) → V) w : V)
Tactic: rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]