k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
hn : Nonempty ι
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
hn : Nonempty ι
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
cases' hn with i0
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
i0 : ι
⊢ ∃ s w x, p1 = ↑(Finset.affineCombination k s p) w
have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction :=
  AffineSubspace.vsub_mem_direction h h0
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
rcases hd with ⟨s, w, h, hs⟩
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
let s' := insert i0 s
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
let w' := Set.indicator (↑s) w
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
have h' : (∑ i in s', w' i) = 0 := by
  rw [← h, Set.sum_indicator_subset _ (Finset.subset_insert i0 s)]
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
  rw [hs]
  exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
let w0 : ι → k := Function.update (Function.const ι 0) i0 1
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
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]
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
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 _ _
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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')
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
use s', w0 + w'
case intro.intro.intro.intro.h
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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')

case intro.intro.intro.intro.w
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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')
constructor
no goals
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
rw [← h, Set.sum_indicator_subset _ (Finset.subset_insert i0 s)]
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
rw [hs]
no goals
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
no goals
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
simp only [Finset.mem_insert, true_or, not_true, Function.const_apply, Finset.sum_const_zero,
  add_zero]
no goals
case intro.intro.intro.intro.h
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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')
rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
case intro.intro.intro.intro.w
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case intro.intro.intro.intro.w
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
change (Finset.sum s' fun i => w0 i + w' i) = 1
no goals
case intro.intro.intro.intro.w
k : Type u_3
V : Type u_4
P : Type u_2
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
simp only [Finset.sum_add_distrib, hw0, h', add_zero]