k : Type u_4
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.352836
s₂✝ : Finset ι₂
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ ↑(weightedVSubOfPoint (s \ s₂) p (Classical.choice (_ : Nonempty P))) w -
      ↑(weightedVSubOfPoint s₂ p (Classical.choice (_ : Nonempty P))) (-w) =
    ↑(weightedVSub s p) w
k : Type u_4
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.352836
s₂✝ : Finset ι₂
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ ↑(affineCombination k (s \ s₂) p) w -ᵥ ↑(affineCombination k s₂ p) (-w) = ↑(weightedVSub s p) w
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
no goals
k : Type u_4
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.352836
s₂✝ : Finset ι₂
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ ↑(weightedVSubOfPoint (s \ s₂) p (Classical.choice (_ : Nonempty P))) w -
      ↑(weightedVSubOfPoint s₂ p (Classical.choice (_ : Nonempty P))) (-w) =
    ↑(weightedVSub s p) w
exact s.weightedVSub_sdiff_sub h _ _