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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
s₁ : s
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have f : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: congr
-- 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
b₁ b₂ : P
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have f : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: ext
-- 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
b₁ b₂ : P
x : ι
| w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have f : w x • (b₂ -ᵥ b₁)
Tactic: rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have f : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
Tactic: ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have f : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
f : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have f₁ : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
Tactic: · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have s₁ : s
Tactic: congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
s₁ : s
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have f : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))) 0
have h₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • (b₂ -ᵥ b₁)) 0
Tactic: conv_lhs =>
    congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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
b₁ b₂ : P
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • (b₂ -ᵥ b₁)) 0
have h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
Tactic: rw [← sum_smul, 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
b₁ b₂ : P
h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • (b₂ -ᵥ b₁)) 0
have h₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (b₂ -ᵥ b₁) = 0
Tactic: rw [← sum_smul, 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
b₁ b₂ : P
h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
h₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (b₂ -ᵥ b₁) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • (b₂ -ᵥ b₁)) 0
have h₃ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [← sum_smul, 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) 1
b₁ b₂ : P
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V) b₁ =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V) b₂
have rw : b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← @vsub_eq_zero_iff_eq V,
    vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← add_sub_assoc, add_comm, add_sub_assoc, ←
    sum_sub_distrib]
-- 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) 1
b₁ b₂ : P
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a : b₁ -ᵥ b₂
Tactic: congr
-- 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) 1
b₁ b₂ : P
a : b₁ -ᵥ b₂
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a₁ : ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
Tactic: congr
-- 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) 1
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a : s
Tactic: congr
-- 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) 1
b₁ b₂ : P
a : s
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a₁ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: congr
-- 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) 1
b₁ b₂ : P
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have a : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: ext
-- 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) 1
b₁ b₂ : P
x : ι
| w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have a : w x • (b₂ -ᵥ b₁)
Tactic: rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have a : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
Tactic: ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have a : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
a : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
have a₁ : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
Tactic: · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a : s
Tactic: congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
a : s
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a₁ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a : s
Tactic: · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
a : s
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a₁ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
Tactic: · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a : b₁ -ᵥ b₂
Tactic: congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
a : b₁ -ᵥ b₂
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
have a₁ : ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
Tactic: congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
have conv_lhs : b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
Tactic: conv_lhs =>
    congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]
-- 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) 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
have rw : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
Tactic: rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
-- 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) 1
b₁ b₂ : P
rw : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
have rw₁ : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (b₂ -ᵥ b₁) = 0
Tactic: rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
-- 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) 1
b₁ b₂ : P
rw : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
rw₁ : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (b₂ -ᵥ b₁) = 0
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
have rw₂ : b₁ -ᵥ b₂ + (b₂ -ᵥ b₁) = 0
Tactic: rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
-- 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) 1
b₁ b₂ : P
rw : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
rw₁ : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (b₂ -ᵥ b₁) = 0
rw₂ : b₁ -ᵥ b₂ + (b₂ -ᵥ b₁) = 0
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
have rw₃ : b₁ -ᵥ b₁ = 0
Tactic: rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
-- 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) 1
b₁ b₂ : P
rw : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
rw₁ : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (b₂ -ᵥ b₁) = 0
rw₂ : b₁ -ᵥ b₂ + (b₂ -ᵥ b₁) = 0
rw₃ : b₁ -ᵥ b₁ = 0
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
have rw₄ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
-- 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 ι
w : ι → k
p : ι → P
i : ι
⊢ Eq.{u_2 + 1} (α := V) (((s.erase i).weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)
have rw : Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
-- 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 ι
w : ι → k
p : ι → P
i : ι
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))
have h : w i • (p i -ᵥ p i) = 0
Tactic: apply sum_erase
-- 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 ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0
have h : HSMul.hSMul (β := V) (w i) 0 = 0
Tactic: rw [vsub_self, smul_zero]
-- 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 ι
w : ι → k
p : ι → P
i : ι
h : HSMul.hSMul (β := V) (w i) 0 = 0
⊢ w i • (p i -ᵥ p i) = 0
have h₁ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [vsub_self, smul_zero]
-- 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 ι
w : ι → k
p : ι → P
i : ι
⊢ Eq.{u_2 + 1} (α := V) (((insert i s).weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)
have rw : Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
-- 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 ι
w : ι → k
p : ι → P
i : ι
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))
have h : w i • (p i -ᵥ p i) = 0
Tactic: apply sum_insert_zero
-- 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
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ Eq.{u_2 + 1} (α := V) ((s₁.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
have rw : Eq.{u_2 + 1} (α := V) (∑ i ∈ s₁, w i • (p i -ᵥ b)) (∑ i ∈ s₂, (↑s₁ : Set ι).indicator w i • (p i -ᵥ b))
Tactic: rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
-- 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
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ Eq.{u_2 + 1} (α := V) (((map e s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s₂.weightedVSubOfPoint (p ∘ (⇑e : (a : ι₂) → ι)) b : (a : ι₂ → k) → V) (w ∘ (⇑e : (a : ι₂) → ι)) : V)
have simp_rw : Eq.{u_2 + 1} (α := V) (∑ i ∈ map e s₂, w i • (p i -ᵥ b))
  (∑ i ∈ s₂, (w ∘ (⇑e : (a : ι₂) → ι)) i • ((p ∘ (⇑e : (a : ι₂) → ι)) i -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply]
-- 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₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
have simp_rw : ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = HSub.hSub (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ b)) (∑ i ∈ s, w i • (p₂ i -ᵥ b))
Tactic: simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]
-- 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
simp_rw : ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = HSub.hSub (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ b)) (∑ i ∈ s, w i • (p₂ i -ᵥ b))
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
have simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) (∑ x ∈ s, (w x • (p₁ x -ᵥ b) - w x • (p₂ x -ᵥ b)))
Tactic: simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]
-- 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
simp_rw : ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = HSub.hSub (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ b)) (∑ i ∈ s, w i • (p₂ i -ᵥ b))
simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) (∑ x ∈ s, (w x • (p₁ x -ᵥ b) - w x • (p₂ x -ᵥ b)))
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
have simp_rw₂ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) (∑ x ∈ s, w x • (p₁ x -ᵥ b - (p₂ x -ᵥ b)))
Tactic: simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]
-- 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₁ 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) (β := 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))
Tactic: rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]