[GOAL]
⊢ univ = {0, 1}
[PROOFSTEP]
ext x
[GOAL]
case a
x : Fin 2
⊢ x ∈ univ ↔ x ∈ {0, 1}
[PROOFSTEP]
fin_cases x
[GOAL]
case a.head
⊢ { val := 0, isLt := (_ : 0 < 2) } ∈ univ ↔ { val := 0, isLt := (_ : 0 < 2) } ∈ {0, 1}
[PROOFSTEP]
simp
[GOAL]
case a.tail.head
⊢ { val := 1, isLt := (_ : (fun a => a < 2) 1) } ∈ univ ↔ { val := 1, isLt := (_ : (fun a => a < 2) 1) } ∈ {0, 1}
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
⊢ ↑(weightedVSubOfPoint s p b) w = ∑ i in s, w i • (p i -ᵥ b)
[PROOFSTEP]
simp [weightedVSubOfPoint, LinearMap.sum_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p b : P
⊢ ↑(weightedVSubOfPoint s (fun x => p) b) w = (∑ i in s, w i) • (p -ᵥ b)
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, sum_smul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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₂
[PROOFSTEP]
simp_rw [weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
refine sum_congr rfl fun i hi => ?_
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
rw [hw i hi, hp i hi]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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₂
[PROOFSTEP]
simp only [Finset.weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
congr
[GOAL]
case e_f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
ext i
[GOAL]
case e_f.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
cases' eq_or_ne i j with h h
[GOAL]
case e_f.h.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
simp [h]
[GOAL]
case e_f.h.inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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)
[PROOFSTEP]
simp [hw i h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  · ext
    rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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₂))
[PROOFSTEP]
  congr
  ·skip
  · ext
    rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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₂))
[PROOFSTEP]
  congr
  ·skip
  · ext
    rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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₂))
[PROOFSTEP]
congr
[GOAL]
case s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| s
case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
·skip
[GOAL]
case s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| s
[PROOFSTEP]
skip
[GOAL]
case s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| s
[PROOFSTEP]
skip
[GOAL]
case s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| s
[PROOFSTEP]
skip
[GOAL]
case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
· ext
  rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
  ext
  rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
  ext
  rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
ext
[GOAL]
case f.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
x✝ : ι
| w x✝ • (p x✝ -ᵥ b₁) - w x✝ • (p x✝ -ᵥ b₂)
[PROOFSTEP]
rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 0
b₁ b₂ : P
⊢ ∑ x in s, w x • (b₂ -ᵥ b₁) = 0
[PROOFSTEP]
rw [← sum_smul, h, zero_smul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
⊢ ↑(weightedVSubOfPoint s p b₁) w +ᵥ b₁ = ↑(weightedVSubOfPoint s p b₂) w +ᵥ b₂
[PROOFSTEP]
erw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← @vsub_eq_zero_iff_eq V, vadd_vsub_assoc,
  vsub_vadd_eq_vsub_sub, ← add_sub_assoc, add_comm, add_sub_assoc, ← sum_sub_distrib]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  · congr
    ·skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂ + ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
  congr
  ·skip
  · congr
    ·skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂ + ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
  congr
  ·skip
  · congr
    ·skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂ + ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
congr
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
·skip
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂
[PROOFSTEP]
skip
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂
[PROOFSTEP]
skip
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| b₁ -ᵥ b₂
[PROOFSTEP]
skip
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
· congr
  ·skip
  · ext
    rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
  congr
  ·skip
  · ext
    rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
  congr
  ·skip
  · ext
    rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| ∑ x in s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
[PROOFSTEP]
congr
[GOAL]
case a.s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| s
case a.f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
·skip
[GOAL]
case a.s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| s
[PROOFSTEP]
skip
[GOAL]
case a.s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| s
[PROOFSTEP]
skip
[GOAL]
case a.s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| s
[PROOFSTEP]
skip
[GOAL]
case a.f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
· ext
  rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case a.f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
  ext
  rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case a.f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
  ext
  rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
case a.f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
| fun x => w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
[PROOFSTEP]
ext
[GOAL]
case a.f.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
x✝ : ι
| w x✝ • (p x✝ -ᵥ b₁) - w x✝ • (p x✝ -ᵥ b₂)
[PROOFSTEP]
rw [← smul_sub, vsub_sub_vsub_cancel_left]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
h : ∑ i in s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x in s, w x • (b₂ -ᵥ b₁) = 0
[PROOFSTEP]
rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ↑(weightedVSubOfPoint (erase s i) p (p i)) w = ↑(weightedVSubOfPoint s p (p i)) w
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 in erase s i, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i)
[PROOFSTEP]
apply sum_erase
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0
[PROOFSTEP]
rw [vsub_self, smul_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ↑(weightedVSubOfPoint (insert i s) p (p i)) w = ↑(weightedVSubOfPoint s p (p i)) w
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ∑ i_1 in insert i s, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i)
[PROOFSTEP]
apply sum_insert_zero
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ w i • (p i -ᵥ p i) = 0
[PROOFSTEP]
rw [vsub_self, smul_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ↑(weightedVSubOfPoint s₁ p b) w = ↑(weightedVSubOfPoint s₂ p b) (Set.indicator (↑s₁) w)
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ∑ i in s₁, w i • (p i -ᵥ b) = ∑ i in s₂, Set.indicator (↑s₁) w i • (p i -ᵥ b)
[PROOFSTEP]
exact Set.sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ↑(weightedVSubOfPoint (map e s₂) p b) w = ↑(weightedVSubOfPoint s₂ (p ∘ ↑e) b) (w ∘ ↑e)
[PROOFSTEP]
simp_rw [weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ∑ i in map e s₂, w i • (p i -ᵥ b) = ∑ i in s₂, (w ∘ ↑e) i • ((p ∘ ↑e) i -ᵥ b)
[PROOFSTEP]
exact Finset.sum_map _ _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₁ p₂ : ι → P
b : P
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂ i) = ↑(weightedVSubOfPoint s p₁ b) w - ↑(weightedVSubOfPoint s p₂ b) w
[PROOFSTEP]
simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₁ : ι → P
p₂ b : P
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂) = ↑(weightedVSubOfPoint s p₁ b) w - (∑ i in s, w i) • (p₂ -ᵥ b)
[PROOFSTEP]
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₂ : ι → P
p₁ b : P
⊢ ∑ i in s, w i • (p₁ -ᵥ p₂ i) = (∑ i in s, w i) • (p₁ -ᵥ b) - ↑(weightedVSubOfPoint s p₂ b) w
[PROOFSTEP]
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂✝ : Finset ι₂
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ↑(weightedVSubOfPoint (s \ s₂) p b) w + ↑(weightedVSubOfPoint s₂ p b) w = ↑(weightedVSubOfPoint s p b) w
[PROOFSTEP]
simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂✝ : Finset ι₂
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ↑(weightedVSubOfPoint (s \ s₂) p b) w - ↑(weightedVSubOfPoint s₂ p b) (-w) = ↑(weightedVSubOfPoint s p b) w
[PROOFSTEP]
rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (↑(weightedVSubOfPoint (Finset.subtype pred s) (fun i => p ↑i) b) fun i => w ↑i) =
    ↑(weightedVSubOfPoint (filter pred s) p b) w
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ↑(weightedVSubOfPoint (filter pred s) p b) w = ↑(weightedVSubOfPoint s p b) w
[PROOFSTEP]
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, sum_filter_of_ne]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ∀ (x : ι), x ∈ s → w x • (p x -ᵥ b) ≠ 0 → pred x
[PROOFSTEP]
intro i hi hne
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ pred i
[PROOFSTEP]
refine' h i hi _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ w i ≠ 0
[PROOFSTEP]
intro hw
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
hw : w i = 0
⊢ False
[PROOFSTEP]
simp [hw] at hne 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
c : k
⊢ ↑(weightedVSubOfPoint s p b) (c • w) = c • ↑(weightedVSubOfPoint s p b) w
[PROOFSTEP]
simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
⊢ ↑(weightedVSub s p) w = ∑ i in s, w i • (p i -ᵥ Classical.choice (_ : Nonempty P))
[PROOFSTEP]
simp [weightedVSub, LinearMap.sum_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : P
h : ∑ i in s, w i = 0
⊢ ↑(weightedVSub s fun x => p) w = 0
[PROOFSTEP]
rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
⊢ ↑(weightedVSub ∅ p) w = 0
[PROOFSTEP]
simp [weightedVSub_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₁ : ι → P
p₂ : P
h : ∑ i in s, w i = 0
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂) = ↑(weightedVSub s p₁) w
[PROOFSTEP]
rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₂ : ι → P
p₁ : P
h : ∑ i in s, w i = 0
⊢ ∑ i in s, w i • (p₁ -ᵥ p₂ i) = -↑(weightedVSub s p₂) w
[PROOFSTEP]
rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
⊢ (fun w => ↑(weightedVSubOfPoint s p (Classical.choice (_ : Nonempty P))) w +ᵥ Classical.choice (_ : Nonempty P))
      (w₂ +ᵥ w₁) =
    ↑(weightedVSub s p) w₂ +ᵥ
      (fun w => ↑(weightedVSubOfPoint s p (Classical.choice (_ : Nonempty P))) w +ᵥ Classical.choice (_ : Nonempty P))
        w₁
[PROOFSTEP]
simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, LinearMap.map_add]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : P
h : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s fun x => p) w = p
[PROOFSTEP]
rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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₂
[PROOFSTEP]
simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w₁ w₂ : ι → k
p : ι → P
⊢ ↑(weightedVSub s p) w₁ +ᵥ ↑(affineCombination k s p) w₂ = ↑(affineCombination k s p) (w₁ + w₂)
[PROOFSTEP]
rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w₁ w₂ : ι → k
p : ι → P
⊢ ↑(affineCombination k s p) w₁ -ᵥ ↑(affineCombination k s p) w₂ = ↑(weightedVSub s p) (w₁ - w₂)
[PROOFSTEP]
rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
⊢ ↑(affineCombination k (attach s) f) (w ∘ f) = ↑(affineCombination k (image f univ) id) w
[PROOFSTEP]
simp only [affineCombination, weightedVSubOfPoint_apply, id.def, vadd_right_cancel_iff, Function.comp_apply,
  AffineMap.coe_mk]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
[PROOFSTEP]
let g₁ : s → V := fun i => w (f i) • (f i -ᵥ Classical.choice S.Nonempty)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
[PROOFSTEP]
let g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice S.Nonempty)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ ∑ x in attach s, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P)) =
    ∑ x in image f univ, w x • (x -ᵥ Classical.choice (_ : Nonempty P))
[PROOFSTEP]
change univ.sum g₁ = (image f univ).sum g₂
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ Finset.sum univ g₁ = Finset.sum (image f univ) g₂
[PROOFSTEP]
have hgf : g₁ = g₂ ∘ f := by
  ext
  simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
⊢ g₁ = g₂ ∘ f
[PROOFSTEP]
ext
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
x✝ : { x // x ∈ s }
⊢ g₁ x✝ = (g₂ ∘ f) x✝
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ Finset.sum univ g₁ = Finset.sum (image f univ) g₂
[PROOFSTEP]
rw [hgf, sum_image]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ Finset.sum univ (g₂ ∘ f) = ∑ x : { x // x ∈ s }, w (f x) • (f x -ᵥ Classical.choice (_ : Nonempty P))
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → ∀ (y : { x // x ∈ s }), y ∈ univ → f x = f y → x = y
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice (_ : Nonempty P))
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice (_ : Nonempty P))
hgf : g₁ = g₂ ∘ f
⊢ ∀ (x : { x // x ∈ s }), x ∈ univ → ∀ (y : { x // x ∈ s }), y ∈ univ → f x = f y → x = y
[PROOFSTEP]
exact fun _ _ _ _ hxy => hf hxy
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset P
w : P → k
⊢ ↑(affineCombination k (attach s) Subtype.val) (w ∘ Subtype.val) = ↑(affineCombination k s id) w
[PROOFSTEP]
classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective, univ_eq_attach,
  attach_image_val]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset P
w : P → k
⊢ ↑(affineCombination k (attach s) Subtype.val) (w ∘ Subtype.val) = ↑(affineCombination k s id) w
[PROOFSTEP]
rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective, univ_eq_attach, attach_image_val]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι✝ : Type u_4
s✝ : Finset ι✝
ι₂ : Type u_5
s₂ : Finset ι₂
ι : Type u_6
s : Finset ι
w : ι → k
p : ι → V
hw : Finset.sum s w = 0
⊢ ↑(weightedVSub s p) w = ∑ i in s, w i • p i
[PROOFSTEP]
simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset ι
p : ι → V
w : ι → k
hw : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s p) w = ∑ i in s, w i • p i
[PROOFSTEP]
simp [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw 0]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
⊢ ↑(affineCombination k s p) w = p i
[PROOFSTEP]
have h1 : ∑ i in s, w i = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ↑(affineCombination k s p) w = p i
[PROOFSTEP]
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i), weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i) +ᵥ p i = p i
[PROOFSTEP]
convert zero_vadd V (p i)
[GOAL]
case h.e'_2.h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∑ i_1 in s, w i_1 • (p i_1 -ᵥ p i) = 0
[PROOFSTEP]
refine sum_eq_zero ?_
[GOAL]
case h.e'_2.h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
⊢ ∀ (x : ι), x ∈ s → w x • (p x -ᵥ p i) = 0
[PROOFSTEP]
intro i2 hi2
[GOAL]
case h.e'_2.h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
⊢ w i2 • (p i2 -ᵥ p i) = 0
[PROOFSTEP]
by_cases h : i2 = i
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → w i2 = 0
h1 : ∑ i in s, w i = 1
i2 : ι
hi2 : i2 ∈ s
h : ¬i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0
[PROOFSTEP]
simp [hw0 i2 hi2 h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂✝ : Finset ι₂
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ ↑(affineCombination k s₁ p) w = ↑(affineCombination k s₂ p) (Set.indicator (↑s₁) w)
[PROOFSTEP]
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_indicator_subset _ _ _ h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
⊢ ↑(affineCombination k (map e s₂) p) w = ↑(affineCombination k s₂ (p ∘ ↑e)) (w ∘ ↑e)
[PROOFSTEP]
simp_rw [affineCombination_apply, weightedVSubOfPoint_map]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂ i) = ↑(affineCombination k s p₁) w -ᵥ ↑(affineCombination k s p₂) w
[PROOFSTEP]
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂ i) =
    ↑(weightedVSubOfPoint s p₁ (Classical.choice (_ : Nonempty P))) w -
      ↑(weightedVSubOfPoint s p₂ (Classical.choice (_ : Nonempty P))) w
[PROOFSTEP]
exact s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₁ : ι → P
p₂ : P
h : ∑ i in s, w i = 1
⊢ ∑ i in s, w i • (p₁ i -ᵥ p₂) = ↑(affineCombination k s p₁) w -ᵥ p₂
[PROOFSTEP]
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p₂ : ι → P
p₁ : P
h : ∑ i in s, w i = 1
⊢ ∑ i in s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ ↑(affineCombination k s p₂) w
[PROOFSTEP]
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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
[PROOFSTEP]
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
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
[PROOFSTEP]
exact s.weightedVSub_sdiff_sub h _ _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ↑(affineCombination k (filter (fun x => x ≠ i) s) p) w = p i
[PROOFSTEP]
classical
rw [← @vsub_eq_zero_iff_eq V, ← hw, ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his),
  sdiff_singleton_eq_erase, ← filter_ne']
congr
refine' (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) _ _).symm
· simp [hwi]
· simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ↑(affineCombination k (filter (fun x => x ≠ i) s) p) w = p i
[PROOFSTEP]
rw [← @vsub_eq_zero_iff_eq V, ← hw, ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his),
  sdiff_singleton_eq_erase, ← filter_ne']
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ↑(affineCombination k (filter (fun x => x ≠ i) s) p) w -ᵥ p i =
    ↑(affineCombination k (filter (fun a => a ≠ i) s) p) w -ᵥ ↑(affineCombination k {i} p) (-w)
[PROOFSTEP]
congr
[GOAL]
case e_a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = ↑(affineCombination k {i} p) (-w)
[PROOFSTEP]
refine' (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) _ _).symm
[GOAL]
case e_a.refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (-w) i = 1
[PROOFSTEP]
simp [hwi]
[GOAL]
case e_a.refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ (i2 : ι), i2 ∈ {i} → i2 ≠ i → (-w) i2 = 0
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (↑(affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) =
    ↑(affineCombination k (filter pred s) p) w
[PROOFSTEP]
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
w : ι → k
p : ι → P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ↑(affineCombination k (filter pred s) p) w = ↑(affineCombination k s p) w
[PROOFSTEP]
rw [affineCombination_apply, affineCombination_apply, s.weightedVSubOfPoint_filter_of_ne _ _ _ h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs x_1 w x, v = ↑(weightedVSubOfPoint fs p b) w) ↔ ∃ fs w x, v = ↑(weightedVSubOfPoint fs (fun i => p ↑i) b) w
[PROOFSTEP]
classical
simp_rw [weightedVSubOfPoint_apply]
constructor
· rintro ⟨fs, hfs, w, rfl, rfl⟩
  exact ⟨fs.subtype s, fun i => w i, sum_subtype_of_mem _ hfs, (sum_subtype_of_mem _ hfs).symm⟩
· rintro ⟨fs, w, rfl, rfl⟩
  refine'
      ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i => if h : i ∈ s then w ⟨i, h⟩ else 0, _,
        _⟩ <;>
    simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs x_1 w x, v = ↑(weightedVSubOfPoint fs p b) w) ↔ ∃ fs w x, v = ↑(weightedVSubOfPoint fs (fun i => p ↑i) b) w
[PROOFSTEP]
simp_rw [weightedVSubOfPoint_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)) ↔ ∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)) → ∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)
[PROOFSTEP]
rintro ⟨fs, hfs, w, rfl, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ι
hfs : ↑fs ⊆ s
w : ι → k
⊢ ∃ fs_1 w_1 h, ∑ i in fs, w i • (p i -ᵥ b) = ∑ i in fs_1, w_1 i • (p ↑i -ᵥ b)
[PROOFSTEP]
exact ⟨fs.subtype s, fun i => w i, sum_subtype_of_mem _ hfs, (sum_subtype_of_mem _ hfs).symm⟩
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)) → ∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)
[PROOFSTEP]
rintro ⟨fs, w, rfl, rfl⟩
[GOAL]
case mpr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∃ fs_1 h w_1 h, ∑ i in fs, w i • (p ↑i -ᵥ b) = ∑ i in fs_1, w_1 i • (p i -ᵥ b)
[PROOFSTEP]
refine' ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i => if h : i ∈ s then w ⟨i, h⟩ else 0, _, _⟩
[GOAL]
case mpr.intro.intro.intro.refine'_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∑ i in map (Function.Embedding.subtype fun x => x ∈ s) fs,
      (fun i => if h : i ∈ s then w { val := i, property := h } else 0) i =
    ∑ i in fs, w i
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.intro.intro.refine'_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∑ i in fs, w i • (p ↑i -ᵥ b) =
    ∑ i in map (Function.Embedding.subtype fun x => x ∈ s) fs,
      (fun i => if h : i ∈ s then w { val := i, property := h } else 0) i • (p i -ᵥ b)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs x w x, p0 = ↑(affineCombination k fs p) w) ↔ ∃ fs w x, p0 = ↑(affineCombination k fs fun i => p ↑i) w
[PROOFSTEP]
simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs h w h,
      p0 -ᵥ Classical.choice (_ : Nonempty P) = ↑(weightedVSubOfPoint fs p (Classical.choice (_ : Nonempty P))) w) ↔
    ∃ fs w h,
      p0 -ᵥ Classical.choice (_ : Nonempty P) =
        ↑(weightedVSubOfPoint fs (fun i => p ↑i) (Classical.choice (_ : Nonempty P))) w
[PROOFSTEP]
exact eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
[PROOFSTEP]
have b := Classical.choice (inferInstance : AffineSpace V P).Nonempty
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
[PROOFSTEP]
have b₂ := Classical.choice (inferInstance : AffineSpace V₂ P₂).Nonempty
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ ↑f (↑(affineCombination k s p) w) = ↑(affineCombination k s (↑f ∘ p)) w
[PROOFSTEP]
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw b,
  s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w (f ∘ p) hw b₂, ←
  s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : Finset.sum s w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ ↑f (↑(weightedVSubOfPoint s p b) w +ᵥ b) = ↑(weightedVSubOfPoint s (↑f ∘ p) (↑f b)) w +ᵥ ↑f b
[PROOFSTEP]
simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd, LinearMap.map_smulₛₗ,
  AffineMap.linearMap_vsub, LinearMap.map_sum, Function.comp_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
⊢ affineCombinationSingleWeights k i i = 1
[PROOFSTEP]
simp [affineCombinationSingleWeights]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0
[PROOFSTEP]
simp [affineCombinationSingleWeights, h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j in s, affineCombinationSingleWeights k i j = 1
[PROOFSTEP]
rw [← affineCombinationSingleWeights_apply_self k i]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
h : i ∈ s
⊢ ∑ j in s, affineCombinationSingleWeights k i j = affineCombinationSingleWeights k i i
[PROOFSTEP]
exact sum_eq_single_of_mem i h fun j _ hj => affineCombinationSingleWeights_apply_of_ne k hj
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
⊢ weightedVSubVSubWeights k i i = 0
[PROOFSTEP]
simp [weightedVSubVSubWeights]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j i = 1
[PROOFSTEP]
simp [weightedVSubVSubWeights, h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j j = -1
[PROOFSTEP]
simp [weightedVSubVSubWeights, h.symm]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
⊢ weightedVSubVSubWeights k i j t = 0
[PROOFSTEP]
simp [weightedVSubVSubWeights, hi, hj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ t in s, weightedVSubVSubWeights k i j t = 0
[PROOFSTEP]
simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ x in s, affineCombinationSingleWeights k i x - ∑ x in s, affineCombinationSingleWeights k j x = 0
[PROOFSTEP]
simp [hi, hj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i : ι
c : k
⊢ affineCombinationLineMapWeights i i c = affineCombinationSingleWeights k i
[PROOFSTEP]
simp [affineCombinationLineMapWeights]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c i = 1 - c
[PROOFSTEP]
simp [affineCombinationLineMapWeights, h.symm, sub_eq_neg_add]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c j = c
[PROOFSTEP]
simp [affineCombinationLineMapWeights, h.symm]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c t = 0
[PROOFSTEP]
simp [affineCombinationLineMapWeights, hi, hj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t in s, affineCombinationLineMapWeights i j c t = 1
[PROOFSTEP]
simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ x in s, (c • weightedVSubVSubWeights k j i) x + ∑ x in s, affineCombinationSingleWeights k i x = 1
[PROOFSTEP]
simp [hi, hj, ← mul_sum]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ ↑(affineCombination k s p) (affineCombinationSingleWeights k i) = p i
[PROOFSTEP]
refine' s.affineCombination_of_eq_one_of_eq_zero _ _ hi (by simp) _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ affineCombinationSingleWeights k i i = 1
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ ∀ (i2 : ι), i2 ∈ s → i2 ≠ i → affineCombinationSingleWeights k i i2 = 0
[PROOFSTEP]
rintro j - hj
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
j : ι
hj : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0
[PROOFSTEP]
simp [hj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ↑(weightedVSub s p) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
[PROOFSTEP]
rw [weightedVSubVSubWeights, ← affineCombination_vsub, s.affineCombination_affineCombinationSingleWeights k p hi,
  s.affineCombination_affineCombinationSingleWeights k p hj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ↑(affineCombination k s p) (affineCombinationLineMapWeights i j c) = ↑(AffineMap.lineMap (p i) (p j)) c
[PROOFSTEP]
rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination, weightedVSub_const_smul,
  s.affineCombination_affineCombinationSingleWeights k p hi, s.weightedVSub_weightedVSubVSubWeights k p hj hi,
  AffineMap.lineMap_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
h : ↑(card s) ≠ 0
⊢ ∑ i in s, centroidWeights k s i = 1
[PROOFSTEP]
simp [h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : CharZero k
h : card s ≠ 0
⊢ ∑ i in s, centroidWeights k s i = 1
[PROOFSTEP]
simp only [centroidWeights_apply, sum_const, nsmul_eq_mul, ne_eq, Nat.cast_eq_zero, card_eq_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : CharZero k
h : card s ≠ 0
⊢ ↑(card s) * (↑(card s))⁻¹ = 1
[PROOFSTEP]
refine mul_inv_cancel ?_
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : CharZero k
h : card s ≠ 0
⊢ ↑(card s) ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset P
⊢ centroid k univ Subtype.val = centroid k s id
[PROOFSTEP]
rw [centroid, centroid, ← s.attach_affineCombination_coe]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset P
⊢ ↑(affineCombination k univ Subtype.val) (centroidWeights k univ) =
    ↑(affineCombination k (attach s) Subtype.val) (centroidWeights k s ∘ Subtype.val)
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset P
⊢ centroidWeights k univ = centroidWeights k s ∘ Subtype.val
[PROOFSTEP]
ext
[GOAL]
case h.e_6.h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s✝ : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
s : Finset P
x✝ : { x // x ∈ s }
⊢ centroidWeights k univ x✝ = (centroidWeights k s ∘ Subtype.val) x✝
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
i : ι
⊢ centroid k {i} p = p i
[PROOFSTEP]
simp [centroid_def, affineCombination_apply]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
[PROOFSTEP]
by_cases h : i₁ = i₂
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
[PROOFSTEP]
simp [h]
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
[PROOFSTEP]
have hc : (card ({ i₁, i₂ } : Finset ι) : k) ≠ 0 :=
  by
  rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
  norm_num
  exact nonzero_of_invertible _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(card {i₁, i₂}) ≠ 0
[PROOFSTEP]
rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ↑(1 + 1) ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ ¬2 = 0
[PROOFSTEP]
exact nonzero_of_invertible _
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(card {i₁, i₂}) ≠ 0
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
[PROOFSTEP]
rw [centroid_def,
  affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
    (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : ↑(card {i₁, i₂}) ≠ 0
⊢ (↑(weightedVSubOfPoint {i₁, i₂} p (p i₁)) fun i => centroidWeights k {i₁, i₂} i) +ᵥ p i₁ =
    2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁
[PROOFSTEP]
simp [h, one_add_one_eq_two]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
[PROOFSTEP]
rw [univ_fin2]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
[PROOFSTEP]
convert centroid_pair k p 0 1
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
p : ι → P
⊢ centroid k (map e s₂) p = centroid k s₂ (p ∘ ↑e)
[PROOFSTEP]
simp [centroid_def, affineCombination_map, centroidWeights]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : card s ≠ 0
⊢ ∑ i : ι, centroidWeightsIndicator k s i = 1
[PROOFSTEP]
rw [sum_centroidWeightsIndicator]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : card s ≠ 0
⊢ ∑ i in s, centroidWeights k s i = 1
[PROOFSTEP]
exact s.sum_centroidWeights_eq_one_of_card_ne_zero k h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : Finset.Nonempty s
⊢ ∑ i : ι, centroidWeightsIndicator k s i = 1
[PROOFSTEP]
rw [sum_centroidWeightsIndicator]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : Finset.Nonempty s
⊢ ∑ i in s, centroidWeights k s i = 1
[PROOFSTEP]
exact s.sum_centroidWeights_eq_one_of_nonempty k h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : card s = n + 1
⊢ ∑ i : ι, centroidWeightsIndicator k s i = 1
[PROOFSTEP]
rw [sum_centroidWeightsIndicator]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
inst✝¹ : CharZero k
inst✝ : Fintype ι
n : ℕ
h : card s = n + 1
⊢ ∑ i in s, centroidWeights k s i = 1
[PROOFSTEP]
exact s.sum_centroidWeights_eq_one_of_card_eq_add_one k h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
let f : p '' ↑s → ι := fun x => x.property.choose
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
have hf : ∀ x, f x ∈ s ∧ p (f x) = x := fun x => x.property.choose_spec
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
let f' : ps → ι := fun x => f ⟨x, hps ▸ x.property⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
have hf' : ∀ x, f' x ∈ s ∧ p (f' x) = x := fun x => hf ⟨x, hps ▸ x.property⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
have hf'i : Function.Injective f' := by
  intro x y h
  rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
⊢ Function.Injective f'
[PROOFSTEP]
intro x y h
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ x = y
[PROOFSTEP]
rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
let f'e : ps ↪ ι := ⟨f', hf'i⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
have hu : Finset.univ.map f'e = s := by
  ext x
  rw [mem_map]
  constructor
  · rintro ⟨i, _, rfl⟩
    exact (hf' i).1
  · intro hx
    use⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
    refine' hi _ (hf' _).1 _ hx _
    rw [(hf' _).2]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
⊢ map f'e univ = s
[PROOFSTEP]
ext x
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ map f'e univ ↔ x ∈ s
[PROOFSTEP]
rw [mem_map]
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ a, a ∈ univ ∧ ↑f'e a = x) ↔ x ∈ s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ a, a ∈ univ ∧ ↑f'e a = x) → x ∈ s
[PROOFSTEP]
rintro ⟨i, _, rfl⟩
[GOAL]
case a.mp.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
i : ↑ps
left✝ : i ∈ univ
⊢ ↑f'e i ∈ s
[PROOFSTEP]
exact (hf' i).1
[GOAL]
case a.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ s → ∃ a, a ∈ univ ∧ ↑f'e a = x
[PROOFSTEP]
intro hx
[GOAL]
case a.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ∃ a, a ∈ univ ∧ ↑f'e a = x
[PROOFSTEP]
use⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ↑f'e { val := p x, property := (_ : p x ∈ ps) } = x
[PROOFSTEP]
refine' hi _ (hf' _).1 _ hx _
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ p (f' { val := p x, property := (_ : p x ∈ ps) }) = p x
[PROOFSTEP]
rw [(hf' _).2]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k s p = centroid k univ fun x => ↑x
[PROOFSTEP]
rw [← hu, centroid_map]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k univ (p ∘ ↑f'e) = centroid k univ fun x => ↑x
[PROOFSTEP]
congr with x
[GOAL]
case e_p.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : ↑ps
⊢ (p ∘ ↑f'e) x = ↑x
[PROOFSTEP]
change p (f' x) = ↑x
[GOAL]
case e_p.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x => Exists.choose (_ : ↑x ∈ p '' ↑s)
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x => f { val := ↑x, property := (_ : ↑x ∈ p '' ↑s) }
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
hf'i : Function.Injective f'
f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : ↑ps
⊢ p (f' x) = ↑x
[PROOFSTEP]
rw [(hf' x).2]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ (i : ι₂), i ∈ s₂ → ∀ (j : ι₂), j ∈ s₂ → p₂ i = p₂ j → i = j
he : p '' ↑s = p₂ '' ↑s₂
⊢ centroid k s p = centroid k s₂ p₂
[PROOFSTEP]
classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl, s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ (i : ι₂), i ∈ s₂ → ∀ (j : ι₂), j ∈ s₂ → p₂ i = p₂ j → i = j
he : p '' ↑s = p₂ '' ↑s₂
⊢ centroid k s p = centroid k s₂ p₂
[PROOFSTEP]
rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl, s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
classical
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
· simp [Finset.eq_empty_of_isEmpty s]
· rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ, Finsupp.mem_span_image_iff_total,
    Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0), Finset.weightedVSubOfPoint_apply]
  let w' := Set.indicator (↑s) w
  have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero
  use Finsupp.onFinset s w' hwx, Set.subset_univ _
  rw [Finsupp.total_apply, Finsupp.onFinset_sum hwx]
  · apply Finset.sum_congr rfl
    intro i hi
    simp [Set.indicator_apply, if_pos hi]
  · exact fun _ => zero_smul k _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
[GOAL]
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
hι : IsEmpty ι
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
simp [Finset.eq_empty_of_isEmpty s]
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ, Finsupp.mem_span_image_iff_total,
  Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0), Finset.weightedVSubOfPoint_apply]
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
⊢ ∃ l,
    l ∈ Finsupp.supported k k Set.univ ∧
      ↑(Finsupp.total ι ((fun x => V) w) k fun i => p i -ᵥ p i0) l = ∑ i in s, w i • (p i -ᵥ p i0)
[PROOFSTEP]
let w' := Set.indicator (↑s) w
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
⊢ ∃ l,
    l ∈ Finsupp.supported k k Set.univ ∧
      ↑(Finsupp.total ι ((fun x => V) w) k fun i => p i -ᵥ p i0) l = ∑ i in s, w i • (p i -ᵥ p i0)
[PROOFSTEP]
have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero
[GOAL]
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∃ l,
    l ∈ Finsupp.supported k k Set.univ ∧
      ↑(Finsupp.total ι ((fun x => V) w) k fun i => p i -ᵥ p i0) l = ∑ i in s, w i • (p i -ᵥ p i0)
[PROOFSTEP]
use Finsupp.onFinset s w' hwx, Set.subset_univ _
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ↑(Finsupp.total ι ((fun x => V) w) k fun i => p i -ᵥ p i0) (Finsupp.onFinset s w' hwx) = ∑ i in s, w i • (p i -ᵥ p i0)
[PROOFSTEP]
rw [Finsupp.total_apply, Finsupp.onFinset_sum hwx]
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∑ a in s, w' a • (p a -ᵥ p i0) = ∑ i in s, w i • (p i -ᵥ p i0)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (x : ι), x ∈ s → w' x • (p x -ᵥ p i0) = w x • (p x -ᵥ p i0)
[PROOFSTEP]
intro i hi
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
i : ι
hi : i ∈ s
⊢ w' i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
[PROOFSTEP]
simp [Set.indicator_apply, if_pos hi]
[GOAL]
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
w' : ι → k := Set.indicator (↑s) w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (a : ι), 0 • (p a -ᵥ p i0) = 0
[PROOFSTEP]
exact fun _ => zero_smul k _
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
classical
have hnz : ∑ i in s, w i ≠ 0 := h.symm ▸ one_ne_zero
have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
cases' hn with i1 hi1
let w1 : ι → k := Function.update (Function.const ι 0) i1 1
have hw1 : ∑ i in s, w1 i = 1 := by
  simp only [Pi.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply, Finset.sum_const_zero, add_zero]
have hw1s : s.affineCombination k p w1 = p i1 :=
  s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_same _ _ _) fun _ _ hne =>
    Function.update_noteq hne _ _
have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction :=
  by
  rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
  apply weightedVSub_mem_vectorSpan
  change (Finset.sum s fun i => w i - w1 i) = 0
  simp only [Finset.sum_sub_distrib, h, hw1, sub_self]
rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have hnz : ∑ i in s, w i ≠ 0 := h.symm ▸ one_ne_zero
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
hn : Finset.Nonempty s
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
cases' hn with i1 hi1
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
let w1 : ι → k := Function.update (Function.const ι 0) i1 1
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have hw1 : ∑ i in s, w1 i = 1 := by
  simp only [Pi.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply, Finset.sum_const_zero, add_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
⊢ ∑ i in s, w1 i = 1
[PROOFSTEP]
simp only [Pi.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply, Finset.sum_const_zero, add_zero]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have hw1s : s.affineCombination k p w1 = p i1 :=
  s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_same _ _ _) fun _ _ hne =>
    Function.update_noteq hne _ _
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction :=
  by
  rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
  apply weightedVSub_mem_vectorSpan
  change (Finset.sum s fun i => w i - w1 i) = 0
  simp only [Finset.sum_sub_distrib, h, hw1, sub_self]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
⊢ ↑(Finset.affineCombination k s p) w -ᵥ p i1 ∈ AffineSubspace.direction (affineSpan k (Set.range p))
[PROOFSTEP]
rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
⊢ ↑(Finset.weightedVSub s p) (w - w1) ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
apply weightedVSub_mem_vectorSpan
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
⊢ ∑ i in s, (w - w1) i = 0
[PROOFSTEP]
change (Finset.sum s fun i => w i - w1 i) = 0
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
⊢ ∑ i in s, (w i - w1 i) = 0
[PROOFSTEP]
simp only [Finset.sum_sub_distrib, h, hw1, sub_self]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
hv : ↑(Finset.affineCombination k s p) w -ᵥ p i1 ∈ AffineSubspace.direction (affineSpan k (Set.range p))
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 1
p : ι → P
hnz : ∑ i in s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i1
hv : ↑(Finset.affineCombination k s p) w -ᵥ p i1 ∈ AffineSubspace.direction (affineSpan k (Set.range p))
⊢ ↑(Finset.affineCombination k s p) w -ᵥ p i1 +ᵥ p i1 ∈ affineSpan k (Set.range p)
[PROOFSTEP]
exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
⊢ v ∈ vectorSpan k (Set.range p) ↔ ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
classical
constructor
· rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
  swap
  · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ, Finsupp.mem_span_image_iff_total]
    rintro ⟨l, _, hv⟩
    use insert i0 l.support
    set w := (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i in l.support, l i) with hwdef
    use w
    have hw : ∑ i in insert i0 l.support, w i = 0 := by
      rw [hwdef]
      simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
        Finset.sum_insert_of_eq_zero_if_not_mem Finsupp.not_mem_support_iff.1]
      simp only [Finsupp.mem_support_iff, ne_eq, Finset.mem_insert, true_or, not_true, Function.const_apply,
        Finset.sum_const_zero, add_zero, sub_self]
    use hw
    have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
    change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz 
    rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0), Finset.weightedVSubOfPoint_apply, ←
      hv, Finsupp.total_apply, @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
    change (∑ i in l.support, l i • _) = _
    congr with i
    by_cases h : i = i0
    · simp [h]
    · simp [hwdef, h]
  · rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
    rintro rfl
    use∅
    simp
· rintro ⟨s, w, hw, rfl⟩
  exact weightedVSub_mem_vectorSpan hw p
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
⊢ v ∈ vectorSpan k (Set.range p) ↔ ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
[GOAL]
case mp.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
hι : IsEmpty ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w x, v = ↑(Finset.weightedVSub s p) w
case mp.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
swap
[GOAL]
case mp.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ, Finsupp.mem_span_image_iff_total]
[GOAL]
case mp.inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
⊢ (∃ l, l ∈ Finsupp.supported k k Set.univ ∧ ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v) →
    ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
rintro ⟨l, _, hv⟩
[GOAL]
case mp.inr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
⊢ ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
use insert i0 l.support
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
⊢ ∃ w x, v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
set w := (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i in l.support, l i) with hwdef
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
⊢ ∃ w x, v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
use w
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
⊢ ∃ x, v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
have hw : ∑ i in insert i0 l.support, w i = 0 := by
  rw [hwdef]
  simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
    Finset.sum_insert_of_eq_zero_if_not_mem Finsupp.not_mem_support_iff.1]
  simp only [Finsupp.mem_support_iff, ne_eq, Finset.mem_insert, true_or, not_true, Function.const_apply,
    Finset.sum_const_zero, add_zero, sub_self]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
⊢ ∑ i in insert i0 l.support, w i = 0
[PROOFSTEP]
rw [hwdef]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
⊢ ∑ i in insert i0 l.support, (↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)) i = 0
[PROOFSTEP]
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
  Finset.sum_insert_of_eq_zero_if_not_mem Finsupp.not_mem_support_iff.1]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
⊢ ∑ x in l.support, ↑l x - (∑ x in l.support, ↑l x + ∑ x in insert i0 l.support \ {i0}, Function.const ι 0 x) = 0
[PROOFSTEP]
simp only [Finsupp.mem_support_iff, ne_eq, Finset.mem_insert, true_or, not_true, Function.const_apply,
  Finset.sum_const_zero, add_zero, sub_self]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
⊢ ∃ x, v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
use hw
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
⊢ v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : w i0 • (p i0 -ᵥ p i0) = 0
⊢ v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz 
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : (fun i => w i • (p i -ᵥ p i0)) i0 = 0
⊢ v = ↑(Finset.weightedVSub (insert i0 l.support) p) w
[PROOFSTEP]
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0), Finset.weightedVSubOfPoint_apply, ← hv,
  Finsupp.total_apply, @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : (fun i => w i • (p i -ᵥ p i0)) i0 = 0
⊢ (Finsupp.sum l fun i a => a • (p i -ᵥ p i0)) = ∑ x in l.support, w x • (p x -ᵥ p i0)
[PROOFSTEP]
change (∑ i in l.support, l i • _) = _
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : (fun i => w i • (p i -ᵥ p i0)) i0 = 0
⊢ ∑ i in l.support, ↑l i • (p i -ᵥ p i0) = ∑ x in l.support, w x • (p x -ᵥ p i0)
[PROOFSTEP]
congr with i
[GOAL]
case h.e_f.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : (fun i => w i • (p i -ᵥ p i0)) i0 = 0
i : ι
⊢ ↑l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
[PROOFSTEP]
by_cases h : i = i0
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : (fun i => w i • (p i -ᵥ p i0)) i0 = 0
i : ι
h : i = i0
⊢ ↑l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : ↑(Finsupp.total ι V k fun i => p i -ᵥ p i0) l = v
w : (a : ι) → (fun x => k) a := ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hwdef : w = ↑l - Function.update (Function.const ι 0) i0 (∑ i in l.support, ↑l i)
hw : ∑ i in insert i0 l.support, w i = 0
hz : (fun i => w i • (p i -ᵥ p i0)) i0 = 0
i : ι
h : ¬i = i0
⊢ ↑l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
[PROOFSTEP]
simp [hwdef, h]
[GOAL]
case mp.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
hι : IsEmpty ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
[GOAL]
case mp.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
hι : IsEmpty ι
⊢ v = 0 → ∃ s w x, v = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
rintro rfl
[GOAL]
case mp.inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
hι : IsEmpty ι
⊢ ∃ s w x, 0 = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
use∅
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
hι : IsEmpty ι
⊢ ∃ w x, 0 = ↑(Finset.weightedVSub ∅ p) w
[PROOFSTEP]
simp
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
v : V
p : ι → P
⊢ (∃ s w x, v = ↑(Finset.weightedVSub s p) w) → v ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
rintro ⟨s, w, hw, rfl⟩
[GOAL]
case mpr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
[PROOFSTEP]
exact weightedVSub_mem_vectorSpan hw p
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
classical
have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn 
cases' hn with i0
have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction := AffineSubspace.vsub_mem_direction h h0
rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd 
rcases hd with ⟨s, w, h, hs⟩
let s' := insert i0 s
let w' := Set.indicator (↑s) w
have h' : ∑ i in s', w' i = 0 := by rw [← h, Set.sum_indicator_subset _ (Finset.subset_insert i0 s)]
have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
  rw [hs]
  exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
let w0 : ι → k := Function.update (Function.const ι 0) i0 1
have hw0 : ∑ i in s', w0 i = 1 :=
  by
  rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
  simp only [Finset.mem_insert, true_or, not_true, Function.const_apply, Finset.sum_const_zero, add_zero]
have hw0s : s'.affineCombination k p w0 = p i0 :=
  s'.affineCombination_of_eq_one_of_eq_zero w0 p (Finset.mem_insert_self _ _) (Function.update_same _ _ _)
    fun _ _ hne => Function.update_noteq hne _ _
use s', w0 + w'
constructor
· rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
·
  -- Porting note: proof was `simp [Pi.add_apply, Finset.sum_add_distrib, hw0, h']`
  change (Finset.sum s' fun i => w0 i + w' i) = 1
  simp only [Finset.sum_add_distrib, hw0, h', add_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
hn : Set.Nonempty ↑(affineSpan k (Set.range p))
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn 
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
hn : Nonempty ι
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
cases' hn with i0
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction := AffineSubspace.vsub_mem_direction h h0
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
hd : p1 -ᵥ p i0 ∈ AffineSubspace.direction (affineSpan k (Set.range p))
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd 
[GOAL]
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
hd : ∃ s w x, p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
rcases hd with ⟨s, w, h, hs⟩
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
let s' := insert i0 s
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
let w' := Set.indicator (↑s) w
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have h' : ∑ i in s', w' i = 0 := by rw [← h, Set.sum_indicator_subset _ (Finset.subset_insert i0 s)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
⊢ ∑ i in s', w' i = 0
[PROOFSTEP]
rw [← h, Set.sum_indicator_subset _ (Finset.subset_insert i0 s)]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
  rw [hs]
  exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
⊢ ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
[PROOFSTEP]
rw [hs]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
⊢ ↑(Finset.weightedVSub s' p) w' = ↑(Finset.weightedVSub s p) w
[PROOFSTEP]
exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
let w0 : ι → k := Function.update (Function.const ι 0) i0 1
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have hw0 : ∑ i in s', w0 i = 1 :=
  by
  rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
  simp only [Finset.mem_insert, true_or, not_true, Function.const_apply, Finset.sum_const_zero, add_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
⊢ ∑ i in s', w0 i = 1
[PROOFSTEP]
rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
⊢ 1 + ∑ x in insert i0 s \ {i0}, Function.const ι 0 x = 1
[PROOFSTEP]
simp only [Finset.mem_insert, true_or, not_true, Function.const_apply, Finset.sum_const_zero, add_zero]
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i in s', w0 i = 1
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
have hw0s : s'.affineCombination k p w0 = p i0 :=
  s'.affineCombination_of_eq_one_of_eq_zero w0 p (Finset.mem_insert_self _ _) (Function.update_same _ _ _)
    fun _ _ hne => Function.update_noteq hne _ _
[GOAL]
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i in s', w0 i = 1
hw0s : ↑(Finset.affineCombination k s' p) w0 = p i0
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
use s', w0 + w'
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i in s', w0 i = 1
hw0s : ↑(Finset.affineCombination k s' p) w0 = p i0
⊢ ∃ x, p1 = ↑(Finset.affineCombination k s' p) (w0 + w')
[PROOFSTEP]
constructor
[GOAL]
case h.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i in s', w0 i = 1
hw0s : ↑(Finset.affineCombination k s' p) w0 = p i0
⊢ p1 = ↑(Finset.affineCombination k s' p) (w0 + w')
[PROOFSTEP]
rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
[GOAL]
case h.w
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i in s', w0 i = 1
hw0s : ↑(Finset.affineCombination k s' p) w0 = p i0
⊢ ∑ i in s', (w0 + w') i = 1
[PROOFSTEP]
change (Finset.sum s' fun i => w0 i + w' i) = 1
[GOAL]
case h.w
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
hs : p1 -ᵥ p i0 = ↑(Finset.weightedVSub s p) w
s' : Finset ι := insert i0 s
w' : ι → k := Set.indicator (↑s) w
h' : ∑ i in s', w' i = 0
hs' : ↑(Finset.weightedVSub s' p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i in s', w0 i = 1
hw0s : ↑(Finset.affineCombination k s' p) w0 = p i0
⊢ ∑ i in s', (w0 i + w' i) = 1
[PROOFSTEP]
simp only [Finset.sum_add_distrib, hw0, h', add_zero]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ w x, p1 = ↑(Finset.affineCombination k Finset.univ p) w
[PROOFSTEP]
classical
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
refine' ⟨(s : Set ι).indicator w, _, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
rw [Fintype.sum_extend_by_zero s w]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ w x, p1 = ↑(Finset.affineCombination k Finset.univ p) w
[PROOFSTEP]
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ w_1 x, ↑(Finset.affineCombination k s p) w = ↑(Finset.affineCombination k Finset.univ p) w_1
[PROOFSTEP]
refine' ⟨(s : Set ι).indicator w, _, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i : ι, Set.indicator (↑s) w i = 1
[PROOFSTEP]
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
[GOAL]
case intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ (∑ x : ι, if x ∈ s then w x else 0) = ∑ i in s, w i
[PROOFSTEP]
rw [Fintype.sum_extend_by_zero s w]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
[PROOFSTEP]
exact eq_affineCombination_of_mem_affineSpan
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ (∃ s w x, p1 = ↑(Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)
[PROOFSTEP]
rintro ⟨s, w, hw, rfl⟩
[GOAL]
case mpr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
⊢ ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
[PROOFSTEP]
exact affineCombination_mem_affineSpan hw p
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
q : P
⊢ q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
q : P
⊢ q ∈ affineSpan k (Set.range p) → ∃ s w, q = ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j
[PROOFSTEP]
intro hq
[GOAL]
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
q : P
hq : q ∈ affineSpan k (Set.range p)
⊢ ∃ s w, q = ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j
[PROOFSTEP]
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq
[GOAL]
case mp.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
hq : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ s_1 w_1, ↑(Finset.affineCombination k s p) w = ↑(Finset.weightedVSubOfPoint s_1 p (p j)) w_1 +ᵥ p j
[PROOFSTEP]
exact ⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩
[GOAL]
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
q : P
⊢ (∃ s w, q = ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j) → q ∈ affineSpan k (Set.range p)
[PROOFSTEP]
rintro ⟨s, w, rfl⟩
[GOAL]
case mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
[PROOFSTEP]
classical
let w' : ι → k := Function.update w j (1 - (s \ { j }).sum w)
have h₁ : (insert j s).sum w' = 1 := by
  by_cases hj : j ∈ s
  · simp [Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
  · simp [Finset.sum_insert hj, Finset.sum_update_of_not_mem hj, hj]
have hww : ∀ i, i ≠ j → w i = w' i := by
  intro i hij
  simp [hij]
rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ← s.weightedVSubOfPoint_insert w' p j, ←
  (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
exact affineCombination_mem_affineSpan h₁ p
[GOAL]
case mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
[PROOFSTEP]
let w' : ι → k := Function.update w j (1 - (s \ { j }).sum w)
[GOAL]
case mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have h₁ : (insert j s).sum w' = 1 := by
  by_cases hj : j ∈ s
  · simp [Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
  · simp [Finset.sum_insert hj, Finset.sum_update_of_not_mem hj, hj]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
⊢ Finset.sum (insert j s) w' = 1
[PROOFSTEP]
by_cases hj : j ∈ s
[GOAL]
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
hj : j ∈ s
⊢ Finset.sum (insert j s) w' = 1
[PROOFSTEP]
simp [Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
[GOAL]
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
hj : ¬j ∈ s
⊢ Finset.sum (insert j s) w' = 1
[PROOFSTEP]
simp [Finset.sum_insert hj, Finset.sum_update_of_not_mem hj, hj]
[GOAL]
case mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
h₁ : Finset.sum (insert j s) w' = 1
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
[PROOFSTEP]
have hww : ∀ i, i ≠ j → w i = w' i := by
  intro i hij
  simp [hij]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
h₁ : Finset.sum (insert j s) w' = 1
⊢ ∀ (i : ι), i ≠ j → w i = w' i
[PROOFSTEP]
intro i hij
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
h₁ : Finset.sum (insert j s) w' = 1
i : ι
hij : i ≠ j
⊢ w i = w' i
[PROOFSTEP]
simp [hij]
[GOAL]
case mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
h₁ : Finset.sum (insert j s) w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
[PROOFSTEP]
rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ← s.weightedVSubOfPoint_insert w' p j, ←
  (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]
[GOAL]
case mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - Finset.sum (s \ {j}) w)
h₁ : Finset.sum (insert j s) w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ ↑(Finset.affineCombination k (insert j s) p) w' ∈ affineSpan k (Set.range p)
[PROOFSTEP]
exact affineCombination_mem_affineSpan h₁ p
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
[PROOFSTEP]
have : s = Set.range ((↑) : s → P) := by simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
⊢ s = Set.range Subtype.val
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s
[PROOFSTEP]
conv_rhs => rw [this]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
| affineSpan k s
[PROOFSTEP]
rw [this]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
| affineSpan k s
[PROOFSTEP]
rw [this]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
| affineSpan k s
[PROOFSTEP]
rw [this]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)
[PROOFSTEP]
apply le_antisymm <;> intro q hq <;>
        erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢ <;>
      obtain ⟨t, μ, rfl⟩ := hq <;>
    use t <;>
  [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)) ≤ affineSpan k (Set.range Subtype.val)
[PROOFSTEP]
intro q hq
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range Subtype.val) ≤ affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
[PROOFSTEP]
intro q hq
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq : q ∈ ↑(affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)))
⊢ q ∈ ↑(affineSpan k (Set.range Subtype.val))
[PROOFSTEP]
erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq : q ∈ ↑(affineSpan k (Set.range Subtype.val))
⊢ q ∈ ↑(affineSpan k (Set.range fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q)))
[PROOFSTEP]
erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq :
  ∃ s_1 w_1,
    q =
      ↑(Finset.weightedVSubOfPoint s_1 (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
              (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
          w_1 +ᵥ
        ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })
⊢ ∃ s_1 w,
    q = ↑(Finset.weightedVSubOfPoint s_1 Subtype.val ↑{ val := p, property := hp }) w +ᵥ ↑{ val := p, property := hp }
[PROOFSTEP]
obtain ⟨t, μ, rfl⟩ := hq
[GOAL]
case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
q : P
hq :
  ∃ s_1 w,
    q = ↑(Finset.weightedVSubOfPoint s_1 Subtype.val ↑{ val := p, property := hp }) w +ᵥ ↑{ val := p, property := hp }
⊢ ∃ s_1 w_1,
    q =
      ↑(Finset.weightedVSubOfPoint s_1 (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
              (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
          w_1 +ᵥ
        ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })
[PROOFSTEP]
obtain ⟨t, μ, rfl⟩ := hq
[GOAL]
case a.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ s_1 w_1,
    ↑(Finset.weightedVSubOfPoint t (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
              (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
          μ +ᵥ
        ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp }) =
      ↑(Finset.weightedVSubOfPoint s_1 Subtype.val ↑{ val := p, property := hp }) w_1 +ᵥ ↑{ val := p, property := hp }
[PROOFSTEP]
use t
[GOAL]
case a.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ s_1 w_1,
    ↑(Finset.weightedVSubOfPoint t Subtype.val ↑{ val := p, property := hp }) μ +ᵥ ↑{ val := p, property := hp } =
      ↑(Finset.weightedVSubOfPoint s_1 (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
              (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
          w_1 +ᵥ
        ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })
[PROOFSTEP]
use t
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ w_1,
    ↑(Finset.weightedVSubOfPoint t (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
              (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
          μ +ᵥ
        ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp }) =
      ↑(Finset.weightedVSubOfPoint t Subtype.val ↑{ val := p, property := hp }) w_1 +ᵥ ↑{ val := p, property := hp }
[PROOFSTEP]
use fun x => μ x * ↑(w x)
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ∃ w_1,
    ↑(Finset.weightedVSubOfPoint t Subtype.val ↑{ val := p, property := hp }) μ +ᵥ ↑{ val := p, property := hp } =
      ↑(Finset.weightedVSubOfPoint t (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
              (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
          w_1 +ᵥ
        ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })
[PROOFSTEP]
use fun x => μ x * ↑(w x)⁻¹
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ↑(Finset.weightedVSubOfPoint t (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
            (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
        μ +ᵥ
      ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp }) =
    (↑(Finset.weightedVSubOfPoint t Subtype.val ↑{ val := p, property := hp }) fun x => μ x * ↑(w x)) +ᵥ
      ↑{ val := p, property := hp }
[PROOFSTEP]
simp [smul_smul]
[GOAL]
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
t : Finset { x // x ∈ s }
μ : { x // x ∈ s } → k
⊢ ↑(Finset.weightedVSubOfPoint t Subtype.val ↑{ val := p, property := hp }) μ +ᵥ ↑{ val := p, property := hp } =
    (↑(Finset.weightedVSubOfPoint t (fun q => ↑(AffineMap.lineMap p ↑q) ↑(w q))
            (↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })))
        fun x => μ x * ↑(w x)⁻¹) +ᵥ
      ↑(AffineMap.lineMap p ↑{ val := p, property := hp }) ↑(w { val := p, property := hp })
[PROOFSTEP]
simp [smul_smul]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
⊢ ∀ (p : (ι → P) × P) (v : (ι → V) × V),
    (fun p => ↑(Finset.weightedVSubOfPoint s p.fst p.snd) w) (v +ᵥ p) =
      ↑(∑ i in s, w i • (LinearMap.comp (LinearMap.proj i) (LinearMap.fst k (ι → V) V) - LinearMap.snd k (ι → V) V))
          v +ᵥ
        (fun p => ↑(Finset.weightedVSubOfPoint s p.fst p.snd) w) p
[PROOFSTEP]
rintro ⟨p, b⟩
  ⟨v, b'⟩
      -- Porting note: needed to give `Prod.mk_vadd_mk` a hint
[GOAL]
case mk.mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
v : ι → V
b' : V
⊢ (fun p => ↑(Finset.weightedVSubOfPoint s p.fst p.snd) w) ((v, b') +ᵥ (p, b)) =
    ↑(∑ i in s, w i • (LinearMap.comp (LinearMap.proj i) (LinearMap.fst k (ι → V) V) - LinearMap.snd k (ι → V) V))
        (v, b') +ᵥ
      (fun p => ↑(Finset.weightedVSubOfPoint s p.fst p.snd) w) (p, b)
[PROOFSTEP]
simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub, ←
  sub_add_eq_add_sub, smul_add, Finset.sum_add_distrib, Prod.mk_vadd_mk v]
