case h
k : Type u_1
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.31556
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
⊢ ↑(weightedVSubOfPoint s p b₁) w - ↑(weightedVSubOfPoint s p b₂) w = 0
k : Type u_1
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.31556
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
⊢ ↑(weightedVSubOfPoint s p b₁) w = ↑(weightedVSubOfPoint s p b₂) w
apply eq_of_sub_eq_zero
case h
k : Type u_1
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.31556
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
⊢ ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
case h
k : Type u_1
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.31556
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
⊢ ↑(weightedVSubOfPoint s p b₁) w - ↑(weightedVSubOfPoint s p b₂) w = 0
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]
no goals
case h
k : Type u_1
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.31556
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
⊢ ∑ x in s, w x • (b₂ -ᵥ b₁) = 0
rw [← sum_smul, h, zero_smul]