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

case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
no goals
case inl
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
simp [Finset.eq_empty_of_isEmpty s]
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
s : Finset ι
w : ι → k
h : ∑ i in s, w i = 0
p : ι → P
i0 : ι
⊢ ↑(Finset.weightedVSub s p) w ∈ vectorSpan k (Set.range p)
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]
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
let w' := Set.indicator (↑s) w
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
use Finsupp.onFinset s w' hwx, Set.subset_univ _
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)

case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
rw [Finsupp.total_apply, Finsupp.onFinset_sum hwx]
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
apply Finset.sum_congr rfl
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
intro i hi
no goals
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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)
simp [Set.indicator_apply, if_pos hi]
no goals
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_1
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
exact fun _ => zero_smul k _