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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
⊢ AffineIndependent k p
intro s w hw hs
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
⊢ ∀ (i : ι), i ∈ s → w i = 0
let p' : { y // y ≠ i } → P := fun x => p x
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ ∀ (i : ι), i ∈ s → w i = 0

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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬(i ∈ s ∧ w i ≠ 0)
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
⊢ ∀ (i : ι), i ∈ s → w i = 0
by_cases his : i ∈ s ∧ w i ≠ 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
refine' False.elim (hi _)
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
let wm : ι → k := -(w i)⁻¹ • w
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
have hms : s.weightedVSub p wm = (0 : V) := by simp [hs]
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
have hwm : (∑ i in s, wm i) = 0 := by simp [← Finset.mul_sum, hw]
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
have hwmi : wm i = -1 := by simp [his.2]
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
let w' : { y // y ≠ i } → k := fun x => wm x
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hw' : ∑ x in s', w' x = 1
⊢ (↑(Finset.affineCombination k (Finset.subtype (fun x => x ≠ i) s) fun i_1 => p ↑i_1) fun i_1 => wm ↑i_1) ∈
    affineSpan k (Set.range (p ∘ Subtype.val))
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hw' : ∑ x in s', w' x = 1
⊢ p i ∈ affineSpan k (p '' {x | x ≠ i})
rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
  (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
  s.affineCombination_subtype_eq_filter]
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hw' : ∑ x in s', w' x = 1
⊢ (↑(Finset.affineCombination k (Finset.subtype (fun x => x ≠ i) s) fun i_1 => p ↑i_1) fun i_1 => wm ↑i_1) ∈
    affineSpan k (Set.range (p ∘ Subtype.val))
exact affineCombination_mem_affineSpan hw' p'
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
⊢ ↑(Finset.weightedVSub s p) wm = 0
simp [hs]
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
⊢ ∑ i in s, wm i = 0
simp [← Finset.mul_sum, hw]
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
⊢ wm i = -1
simp [his.2]
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ i in s, wm i = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
⊢ ∑ x in s', w' x = 1
simp_rw [Finset.sum_subtype_eq_sum_filter]
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm :
  ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x +
      ∑ x in Finset.filter (fun x => x = i) s, (-(w i)⁻¹ • w) x =
    0
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwm : ∑ x in Finset.filter (fun x => x ≠ i) s, wm x + ∑ x in Finset.filter (fun x => ¬x ≠ i) s, wm x = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
simp_rw [Classical.not_not] at hwm
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm : ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x + ∑ x in if i ∈ s then {i} else ∅, (-(w i)⁻¹ • w) x = 0
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm :
  ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x +
      ∑ x in Finset.filter (fun x => x = i) s, (-(w i)⁻¹ • w) x =
    0
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
erw [Finset.filter_eq'] at hwm
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm : ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm : ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x + ∑ x in if i ∈ s then {i} else ∅, (-(w i)⁻¹ • w) x = 0
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
simp_rw [if_pos his.1, Finset.sum_singleton, hwmi, ← sub_eq_add_neg, sub_eq_zero] at hwm
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : ↑(Finset.weightedVSub s p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm : ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, (-(w i)⁻¹ • w) x = 1
exact hwm
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬(i ∈ s ∧ w i ≠ 0)
⊢ ∀ (i : ι), i ∈ s → w i = 0
rw [not_and_or, Classical.not_not] at his
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
let w' : { y // y ≠ i } → k := fun x => w x
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∀ (i : ι), i ∈ s → w i = 0
have hw' : (∑ x in s', w' x) = 0 := by
  simp_rw [Finset.sum_subtype_eq_sum_filter]
  rw [Finset.sum_filter_of_ne, hw]
  rintro x hxs hwx rfl
  exact hwx (his.neg_resolve_left hxs)
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
have hs' : s'.weightedVSub p' w' = (0 : V) := by
  simp_rw [Finset.weightedVSub_subtype_eq_filter]
  rw [Finset.weightedVSub_filter_of_ne, hs]
  rintro x hxs hwx rfl
  exact hwx (his.neg_resolve_left hxs)
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : j ∈ s
⊢ w j = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
⊢ ∀ (i : ι), i ∈ s → w i = 0
intro j hj
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : j ∈ s
hji : j = i
⊢ w j = 0

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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : j ∈ s
hji : ¬j = i
⊢ w j = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : j ∈ s
⊢ w j = 0
by_cases hji : j = i
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, w x = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∑ x in s', w' x = 0
simp_rw [Finset.sum_subtype_eq_sum_filter]
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∀ (x : ι), x ∈ s → w x ≠ 0 → x ≠ i
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∑ x in Finset.filter (fun x => x ≠ i) s, w x = 0
rw [Finset.sum_filter_of_ne, hw]
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
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent k fun x_1 => p ↑x_1
hi : ¬p x ∈ affineSpan k (p '' {x_1 | x_1 ≠ x})
s' : Finset { y // y ≠ x } := Finset.subtype (fun x_1 => x_1 ≠ x) s
p' : { y // y ≠ x } → P := fun x_1 => p ↑x_1
his : ¬x ∈ s ∨ w x = 0
w' : { y // y ≠ x } → k := fun x_1 => w ↑x_1
⊢ False
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∀ (x : ι), x ∈ s → w x ≠ 0 → x ≠ i
rintro x hxs hwx rfl
no goals
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
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent k fun x_1 => p ↑x_1
hi : ¬p x ∈ affineSpan k (p '' {x_1 | x_1 ≠ x})
s' : Finset { y // y ≠ x } := Finset.subtype (fun x_1 => x_1 ≠ x) s
p' : { y // y ≠ x } → P := fun x_1 => p ↑x_1
his : ¬x ∈ s ∨ w x = 0
w' : { y // y ≠ x } → k := fun x_1 => w ↑x_1
⊢ False
exact hwx (his.neg_resolve_left hxs)
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ↑(Finset.weightedVSub (Finset.filter (fun x => x ≠ i) s) p) w = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ↑(Finset.weightedVSub s' p') w' = 0
simp_rw [Finset.weightedVSub_subtype_eq_filter]
case 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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ∀ (i_1 : ι), i_1 ∈ s → w i_1 ≠ 0 → i_1 ≠ i
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ↑(Finset.weightedVSub (Finset.filter (fun x => x ≠ i) s) p) w = 0
rw [Finset.weightedVSub_filter_of_ne, hs]
case 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
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent k fun x_1 => p ↑x_1
hi : ¬p x ∈ affineSpan k (p '' {x_1 | x_1 ≠ x})
s' : Finset { y // y ≠ x } := Finset.subtype (fun x_1 => x_1 ≠ x) s
p' : { y // y ≠ x } → P := fun x_1 => p ↑x_1
his : ¬x ∈ s ∨ w x = 0
w' : { y // y ≠ x } → k := fun x_1 => w ↑x_1
hw' : ∑ x in s', w' x = 0
⊢ False
case 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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
⊢ ∀ (i_1 : ι), i_1 ∈ s → w i_1 ≠ 0 → i_1 ≠ i
rintro x hxs hwx rfl
no goals
case 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
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent k fun x_1 => p ↑x_1
hi : ¬p x ∈ affineSpan k (p '' {x_1 | x_1 ≠ x})
s' : Finset { y // y ≠ x } := Finset.subtype (fun x_1 => x_1 ≠ x) s
p' : { y // y ≠ x } → P := fun x_1 => p ↑x_1
his : ¬x ∈ s ∨ w x = 0
w' : { y // y ≠ x } → k := fun x_1 => w ↑x_1
hw' : ∑ x in s', w' x = 0
⊢ False
exact hwx (his.neg_resolve_left hxs)
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : i ∈ s
hji : j = i
⊢ w j = 0
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : j ∈ s
hji : j = i
⊢ w j = 0
rw [hji] at hj
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : i ∈ s
hji : j = i
⊢ w j = 0
exact hji.symm ▸ his.neg_resolve_left hj
no goals
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
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : ¬p i ∈ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : ¬i ∈ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x in s', w' x = 0
hs' : ↑(Finset.weightedVSub s' p') w' = 0
j : ι
hj : j ∈ s
hji : ¬j = i
⊢ w j = 0
exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)