k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ ∑ i in s, w₁ i • (p i -ᵥ p j) = ∑ i in s, w₂ i • (p i -ᵥ p j)
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ ↑(weightedVSubOfPoint s p (p j)) w₁ = ↑(weightedVSubOfPoint s p (p j)) w₂
simp only [Finset.weightedVSubOfPoint_apply]
case e_f
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ (fun i => w₁ i • (p i -ᵥ p j)) = fun i => w₂ i • (p i -ᵥ p j)
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ ∑ i in s, w₁ i • (p i -ᵥ p j) = ∑ i in s, w₂ i • (p i -ᵥ p j)
congr
case e_f.h
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
case e_f
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ (fun i => w₁ i • (p i -ᵥ p j)) = fun i => w₂ i • (p i -ᵥ p j)
ext i
case e_f.h.inl
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i = j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

case e_f.h.inr
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i ≠ j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
case e_f.h
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
cases' eq_or_ne i j with h h
no goals
case e_f.h.inl
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i = j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
simp [h]
no goals
case e_f.h.inr
k : Type u_2
V : Type u_3
P : Type u_4
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.26193
s₂ : Finset ι₂
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i ≠ j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
simp [hw i h]