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.22097
s₂ : Finset ι₂
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ∈ s → w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ (i : ι), i ∈ s → p₁ i = p₂ i
b : P
⊢ ∑ i in s, w₁ i • (p₁ i -ᵥ b) = ∑ i in s, w₂ i • (p₂ i -ᵥ b)
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.22097
s₂ : Finset ι₂
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ∈ s → w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ (i : ι), i ∈ s → p₁ i = p₂ i
b : P
⊢ ↑(weightedVSubOfPoint s p₁ b) w₁ = ↑(weightedVSubOfPoint s p₂ b) w₂
simp_rw [weightedVSubOfPoint_apply]
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.22097
s₂ : Finset ι₂
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ∈ s → w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ (i : ι), i ∈ s → p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
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.22097
s₂ : Finset ι₂
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ∈ s → w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ (i : ι), i ∈ s → p₁ i = p₂ i
b : P
⊢ ∑ i in s, w₁ i • (p₁ i -ᵥ b) = ∑ i in s, w₂ i • (p₂ i -ᵥ b)
refine sum_congr rfl fun i hi => ?_
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.22097
s₂ : Finset ι₂
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ∈ s → w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ (i : ι), i ∈ s → p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
rw [hw i hi, hp i hi]