case mp
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
inst✝ : Fintype ι
p : ι → P
⊢ AffineIndependent k p →
    ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0

case mpr
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
inst✝ : Fintype ι
p : ι → P
⊢ (∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0) →
    AffineIndependent k 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
inst✝ : Fintype ι
p : ι → P
⊢ AffineIndependent k p ↔
    ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0
constructor
no goals
case mp
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
inst✝ : Fintype ι
p : ι → P
⊢ AffineIndependent k p →
    ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0
exact fun h w hw hs i => h Finset.univ w hw hs i (Finset.mem_univ _)
case mpr
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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w 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_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
inst✝ : Fintype ι
p : ι → P
⊢ (∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0) →
    AffineIndependent k p
intro h s w hw hs i hi
case mpr
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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub Finset.univ p) (Set.indicator (↑s) w) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
case mpr
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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w 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_indicator_subset _ _ (Finset.subset_univ s)] at hs
case mpr
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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i : ι, Set.indicator (↑s) (fun i => w i) i = 0
hs : ↑(Finset.weightedVSub Finset.univ p) (Set.indicator (↑s) w) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
case mpr
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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub Finset.univ p) (Set.indicator (↑s) w) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
rw [Set.sum_indicator_subset _ (Finset.subset_univ s)] at hw
case mpr
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
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i : ι, Set.indicator (↑s) (fun i => w i) i = 0
hs : ↑(Finset.weightedVSub Finset.univ p) (Set.indicator (↑s) w) = 0
i : ι
hi : i ∈ s
h : Set.indicator (↑s) w i = 0
⊢ w i = 0
case mpr
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
inst✝ : Fintype ι
p : ι → P
h : ∀ (w : ι → k), ∑ i : ι, w i = 0 → ↑(Finset.weightedVSub Finset.univ p) w = 0 → ∀ (i : ι), w i = 0
s : Finset ι
w : ι → k
hw : ∑ i : ι, Set.indicator (↑s) (fun i => w i) i = 0
hs : ↑(Finset.weightedVSub Finset.univ p) (Set.indicator (↑s) w) = 0
i : ι
hi : i ∈ s
⊢ w i = 0
replace h := h ((↑s : Set ι).indicator w) hw hs i
no goals
case mpr
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
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i : ι, Set.indicator (↑s) (fun i => w i) i = 0
hs : ↑(Finset.weightedVSub Finset.univ p) (Set.indicator (↑s) w) = 0
i : ι
hi : i ∈ s
h : Set.indicator (↑s) w i = 0
⊢ w i = 0
simpa [hi] using h