case mp
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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

case mpr
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
constructor
case mp
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
case mp
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
intro hq
case mp.intro.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
case mp
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan hq
no goals
case mp.intro.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
exact ⟨s, w, s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw (p j)⟩
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
case mpr
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
rintro ⟨s, w, rfl⟩
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
⊢ ↑(Finset.weightedVSubOfPoint s p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
let w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
have hww : ∀ i, i ≠ j → w i = w' i := by
  intro i hij
  simp [hij]
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
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)]
no goals
case mpr.intro.intro
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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)
exact affineCombination_mem_affineSpan h₁ p
case pos
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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

case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
by_cases hj : j ∈ s
no goals
case pos
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
simp [Finset.sum_update_of_mem hj, Finset.insert_eq_of_mem hj]
no goals
case neg
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
simp [Finset.sum_insert hj, Finset.sum_update_of_not_mem hj, hj]
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
intro i hij
no goals
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
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
simp [hij]