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
p : ι → P
i1 : ι
⊢ AffineIndependent k p → LinearIndependent k fun i => p ↑i -ᵥ p i1

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
p : ι → P
i1 : ι
⊢ (LinearIndependent k fun i => p ↑i -ᵥ p i1) → AffineIndependent k p
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
i1 : ι
⊢ AffineIndependent k p ↔ LinearIndependent k fun i => p ↑i -ᵥ p i1
constructor
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
p : ι → P
i1 : ι
h : AffineIndependent k p
⊢ LinearIndependent k fun i => p ↑i -ᵥ p i1
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
p : ι → P
i1 : ι
⊢ AffineIndependent k p → LinearIndependent k fun i => p ↑i -ᵥ p i1
intro h
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
p : ι → P
i1 : ι
h : AffineIndependent k p
⊢ ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
⊢ LinearIndependent k fun i => p ↑i -ᵥ p i1
rw [linearIndependent_iff']
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
⊢ g i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
⊢ ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
intro s g hg i hi
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
⊢ g i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
⊢ g i = 0
set f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g ⟨x, hx⟩ with hfdef
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
⊢ g i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
⊢ g i = 0
let s2 : Finset ι := insert i1 (s.map (Embedding.subtype _))
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ g i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
⊢ g i = 0
have hfg : ∀ x : { x // x ≠ i1 }, g x = f x := by
  intro x
  rw [hfdef]
  dsimp only
  erw [dif_neg x.property, Subtype.coe_eta]
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f ↑i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ g i = 0
rw [hfg]
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
⊢ f ↑i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f ↑i = 0
have hf : (∑ ι in s2, f ι) = 0 := by
  rw [Finset.sum_insert
      (Finset.not_mem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
    Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]
  rw [hfdef]
  dsimp only
  rw [dif_pos rfl]
  exact neg_add_self _
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
hs2 : ↑(Finset.weightedVSub s2 p) f = 0
⊢ f ↑i = 0
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
⊢ f ↑i = 0
have hs2 : s2.weightedVSub p f = (0 : V) := by
  set f2 : ι → V := fun x => f x • (p x -ᵥ p i1) with hf2def
  set g2 : { x // x ≠ i1 } → V := fun x => g x • (p x -ᵥ p i1)
  have hf2g2 : ∀ x : { x // x ≠ i1 }, f2 x = g2 x := by
    simp only [hf2def]
    refine' fun x => _
    rw [hfg]
  rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s2 f p hf (p i1),
    Finset.weightedVSubOfPoint_insert, Finset.weightedVSubOfPoint_apply,
    Finset.sum_subtype_map_embedding fun x _ => hf2g2 x]
  exact hg
no goals
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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
hs2 : ↑(Finset.weightedVSub s2 p) f = 0
⊢ f ↑i = 0
exact h s2 f hf hs2 i (Finset.mem_insert_of_mem (Finset.mem_map.2 ⟨i, hi, rfl⟩))
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = f ↑x
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
⊢ ∀ (x : { x // x ≠ i1 }), g x = f ↑x
intro x
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = (fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }) ↑x
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = f ↑x
rw [hfdef]
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = if hx : ↑x = i1 then -∑ y in s, g y else g { val := ↑x, property := hx }
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = (fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }) ↑x
dsimp only
no goals
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
x : { x // x ≠ i1 }
⊢ g x = if hx : ↑x = i1 then -∑ y in s, g y else g { val := ↑x, property := hx }
erw [dif_neg x.property, Subtype.coe_eta]
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f i1 + ∑ x in s, g x = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ ∑ ι in s2, f ι = 0
rw [Finset.sum_insert
    (Finset.not_mem_map_subtype_of_not_property s (Classical.not_not.2 rfl)),
  Finset.sum_subtype_map_embedding fun x _ => (hfg x).symm]
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ (fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }) i1 + ∑ x in s, g x = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f i1 + ∑ x in s, g x = 0
rw [hfdef]
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ (if hx : i1 = i1 then -∑ y in s, g y else g { val := i1, property := hx }) + ∑ x in s, g x = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ (fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }) i1 + ∑ x in s, g x = 0
dsimp only
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ -∑ y in s, g y + ∑ x in s, g x = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ (if hx : i1 = i1 then -∑ y in s, g y else g { val := i1, property := hx }) + ∑ x in s, g x = 0
rw [dif_pos rfl]
no goals
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ -∑ y in s, g y + ∑ x in s, g x = 0
exact neg_add_self _
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
⊢ ↑(Finset.weightedVSub s2 p) f = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
⊢ ↑(Finset.weightedVSub s2 p) f = 0
set f2 : ι → V := fun x => f x • (p x -ᵥ p i1) with hf2def
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
⊢ ↑(Finset.weightedVSub s2 p) f = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
⊢ ↑(Finset.weightedVSub s2 p) f = 0
set g2 : { x // x ≠ i1 } → V := fun x => g x • (p x -ᵥ p i1)
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ↑(Finset.weightedVSub s2 p) f = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
⊢ ↑(Finset.weightedVSub s2 p) f = 0
have hf2g2 : ∀ x : { x // x ≠ i1 }, f2 x = g2 x := by
  simp only [hf2def]
  refine' fun x => _
  rw [hfg]
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ∑ x in s, g2 x = 0
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ↑(Finset.weightedVSub s2 p) f = 0
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s2 f p hf (p i1),
  Finset.weightedVSubOfPoint_insert, Finset.weightedVSubOfPoint_apply,
  Finset.sum_subtype_map_embedding fun x _ => hf2g2 x]
no goals
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ∑ x in s, g2 x = 0
exact hg
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
⊢ ∀ (x : { x // x ≠ i1 }),
    (if hx : ↑x = i1 then -∑ y in s, g y else g { val := ↑x, property := hx }) • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
⊢ ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
simp only [hf2def]
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
x : { x // x ≠ i1 }
⊢ (if hx : ↑x = i1 then -∑ y in s, g y else g { val := ↑x, property := hx }) • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
⊢ ∀ (x : { x // x ≠ i1 }),
    (if hx : ↑x = i1 then -∑ y in s, g y else g { val := ↑x, property := hx }) • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)
refine' fun x => _
no goals
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
hfdef : f = fun x => if hx : x = i1 then -∑ y in s, g y else g { val := x, property := hx }
s2 : Finset ι := insert i1 (Finset.map (Embedding.subtype fun x => x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι in s2, f ι = 0
f2 : ι → V := fun x => f x • (p x -ᵥ p i1)
hf2def : f2 = fun x => f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x => g x • (p ↑x -ᵥ p i1)
hg : Finset.sum s g2 = 0
x : { x // x ≠ i1 }
⊢ (if hx : ↑x = i1 then -∑ y in s, g y else g { val := ↑x, property := hx }) • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)
rw [hfg]
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
p : ι → P
i1 : ι
h : LinearIndependent k fun i => p ↑i -ᵥ p i1
⊢ AffineIndependent k p
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
p : ι → P
i1 : ι
⊢ (LinearIndependent k fun i => p ↑i -ᵥ p i1) → AffineIndependent k p
intro h
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
⊢ AffineIndependent k p
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
p : ι → P
i1 : ι
h : LinearIndependent k fun i => p ↑i -ᵥ p i1
⊢ AffineIndependent k p
rw [linearIndependent_iff'] at h
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
⊢ AffineIndependent k p
intro s w hw hs i hi
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p hw (p i1), ←
  s.weightedVSubOfPoint_erase w p i1, Finset.weightedVSubOfPoint_apply] at hs
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
let f : ι → V := fun i => w i • (p i -ᵥ p i1)
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
⊢ w i = 0
have hs2 : (∑ i in (s.erase i1).subtype fun i => i ≠ i1, f i) = 0 := by
  rw [← hs]
  convert Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), i ∈ Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1) → (fun x => w ↑x) i = 0
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
⊢ w i = 0
have h2 := h ((s.erase i1).subtype fun i => i ≠ i1) (fun x => w x) hs2
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ Finset.erase s i1 → w ↑i = 0
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), i ∈ Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1) → (fun x => w ↑x) i = 0
⊢ w i = 0
simp_rw [Finset.mem_subtype] at h2
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ Finset.erase s i1 → w ↑i = 0
h2b : ∀ (i : ι), i ∈ s → i ≠ i1 → w i = 0
⊢ w i = 0
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ Finset.erase s i1 → w ↑i = 0
⊢ w i = 0
have h2b : ∀ i ∈ s, i ≠ i1 → w i = 0 := fun i his hi =>
  h2 ⟨i, hi⟩ (Finset.mem_erase_of_ne_of_mem hi his)
no goals
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
p : ι → P
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
hs2 : ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ Finset.erase s i1 → w ↑i = 0
h2b : ∀ (i : ι), i ∈ s → i ≠ i1 → w i = 0
⊢ w i = 0
exact Finset.eq_zero_of_sum_eq_zero hw h2b i hi
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
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
⊢ ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1)
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
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
⊢ ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = 0
rw [← hs]
no goals
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
i1 : ι
h :
  ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k),
    ∑ i in s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ (i : { x // x ≠ i1 }), i ∈ s → g i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i => w i • (p i -ᵥ p i1)
⊢ ∑ i in Finset.subtype (fun i => i ≠ i1) (Finset.erase s i1), f ↑i = ∑ i in Finset.erase s i1, w i • (p i -ᵥ p i1)
convert Finset.sum_subtype_of_mem f fun x => Finset.ne_of_mem_erase