no goals
k : Type u_2
V : Type u_4
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.251934
s₂ : Finset ι₂
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ∈ s → w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ (i : ι), i ∈ s → p₁ i = p₂ i
⊢ ↑(affineCombination k s p₁) w₁ = ↑(affineCombination k s p₂) w₂
simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]