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
⊢ AffineIndependent k p →
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i in s1, w1 i = 1 →
        ∑ i in s2, w2 i = 1 →
          ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
            Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2

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
⊢ (∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i in s1, w1 i = 1 →
        ∑ i in s2, w2 i = 1 →
          ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
            Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2) →
    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
⊢ AffineIndependent k p ↔
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i in s1, w1 i = 1 →
        ∑ i in s2, w2 i = 1 →
          ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
            Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
⊢ Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
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
⊢ AffineIndependent k p →
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i in s1, w1 i = 1 →
        ∑ i in s2, w2 i = 1 →
          ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
            Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
intro ha s1 s2 w1 w2 hw1 hw2 heq
case mp.h
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
⊢ Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
ext i
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i

case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
case mp.h
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
by_cases hi : i ∈ s1 ∪ s2
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
rw [← sub_eq_zero]
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
rw [Set.sum_indicator_subset _ (Finset.subset_union_left s1 s2)] at hw1
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
rw [Set.sum_indicator_subset _ (Finset.subset_union_right s1 s2)] at hw2
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i = 0
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
have hws : (∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
  simp [hw1, hw2]
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.weightedVSub (s1 ∪ s2) p) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) = 0
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i = 0
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i = 0
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
rw [Finset.affineCombination_indicator_subset _ _ (Finset.subset_union_left s1 s2),
  Finset.affineCombination_indicator_subset _ _ (Finset.subset_union_right s1 s2),
  ← @vsub_eq_zero_iff_eq V, Finset.affineCombination_vsub] at heq
no goals
case pos
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.weightedVSub (s1 ∪ s2) p) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) = 0
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i = 0
⊢ Set.indicator (↑s1) w1 i - Set.indicator (↑s2) w2 i = 0
exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1 ∪ s2, Set.indicator (↑s1) (fun i => w1 i) i = 1
hw2 : ∑ i in s1 ∪ s2, Set.indicator (↑s2) (fun i => w2 i) i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ ∑ i in s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i = 0
simp [hw1, hw2]
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ s1 ∪ s2
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
rw [← Finset.mem_coe, Finset.coe_union] at hi
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
have h₁ : Set.indicator (↑s1) w1 i = 0 := by
  simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
  intro h
  by_contra
  exact (mt (@Set.mem_union_left _ i ↑s1 ↑s2) hi) h
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
h₂ : Set.indicator (↑s2) w2 i = 0
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
have h₂ : Set.indicator (↑s2) w2 i = 0 := by
  simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
  intro h
  by_contra
  exact ( mt (@Set.mem_union_right _ i ↑s2 ↑s1) hi) h
no goals
case neg
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
h₂ : Set.indicator (↑s2) w2 i = 0
⊢ Set.indicator (↑s1) w1 i = Set.indicator (↑s2) w2 i
simp [h₁, h₂]
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
⊢ i ∈ s1 → w1 i = 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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
⊢ Set.indicator (↑s1) w1 i = 0
simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h : i ∈ s1
⊢ w1 i = 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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
⊢ i ∈ s1 → w1 i = 0
intro h
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h : i ∈ s1
x✝ : ¬w1 i = 0
⊢ False
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h : i ∈ s1
⊢ w1 i = 0
by_contra
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h : i ∈ s1
x✝ : ¬w1 i = 0
⊢ False
exact (mt (@Set.mem_union_left _ i ↑s1 ↑s2) hi) h
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
⊢ i ∈ s2 → w2 i = 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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
⊢ Set.indicator (↑s2) w2 i = 0
simp only [Set.indicator, Finset.mem_coe, ite_eq_right_iff]
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
h : i ∈ s2
⊢ w2 i = 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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
⊢ i ∈ s2 → w2 i = 0
intro h
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
h : i ∈ s2
x✝ : ¬w2 i = 0
⊢ False
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
h : i ∈ s2
⊢ w2 i = 0
by_contra
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
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i in s1, w1 i = 1
hw2 : ∑ i in s2, w2 i = 1
heq : ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2
i : ι
hi : ¬i ∈ ↑s1 ∪ ↑s2
h₁ : Set.indicator (↑s1) w1 i = 0
h : i ∈ s2
x✝ : ¬w2 i = 0
⊢ False
exact ( mt (@Set.mem_union_right _ i ↑s2 ↑s1) hi) 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
⊢ w i0 = 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
⊢ (∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      ∑ i in s1, w1 i = 1 →
        ∑ i in s2, w2 i = 1 →
          ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
            Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2) →
    AffineIndependent k p
intro ha s w hw hs i0 hi0
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
⊢ w i0 = 0
let w1 : ι → k := Function.update (Function.const ι 0) i0 1
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ w i0 = 0
have hw1 : (∑ i in s, w1 i) = 1 := by
  rw [Finset.sum_update_of_mem hi0]
  simp only [Finset.sum_const_zero, add_zero, const_apply]
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
⊢ w i0 = 0
have hw1s : s.affineCombination k p w1 = p i0 :=
  s.affineCombination_of_eq_one_of_eq_zero w1 p hi0 (Function.update_same _ _ _)
    fun _ _ hne => Function.update_noteq hne _ _
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
⊢ w i0 = 0
let w2 := w + w1
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
⊢ w i0 = 0
have hw2 : (∑ i in s, w2 i) = 1 := by
  simp_all only [Pi.add_apply, Finset.sum_add_distrib, zero_add]
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
⊢ w i0 = 0
have hw2s : s.affineCombination k p w2 = p i0 := by
  simp_all only [← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
⊢ w i0 = 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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
⊢ w i0 = 0
replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
hws : w2 i0 - w1 i0 = 0
⊢ w i0 = 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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
⊢ w i0 = 0
have hws : w2 i0 - w1 i0 = 0 := by
  rw [← Finset.mem_coe] at hi0
  rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
hws : w2 i0 - w1 i0 = 0
⊢ w i0 = 0
simpa using hws
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ 1 + ∑ x in s \ {i0}, const ι 0 x = 1
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ ∑ i in s, w1 i = 1
rw [Finset.sum_update_of_mem hi0]
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ 1 + ∑ x in s \ {i0}, const ι 0 x = 1
simp only [Finset.sum_const_zero, add_zero, const_apply]
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
⊢ ∑ i in s, w2 i = 1
simp_all only [Pi.add_apply, Finset.sum_add_distrib, zero_add]
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
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    ∑ i in s1, w1 i = 1 →
      ∑ i in s2, w2 i = 1 →
        ↑(Finset.affineCombination k s1 p) w1 = ↑(Finset.affineCombination k s2 p) w2 →
          Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
⊢ ↑(Finset.affineCombination k s p) w2 = p i0
simp_all only [← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ ↑s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
⊢ w2 i0 - w1 i0 = 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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
⊢ w2 i0 - w1 i0 = 0
rw [← Finset.mem_coe] at hi0
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
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
hs : ↑(Finset.weightedVSub s p) w = 0
i0 : ι
hi0 : i0 ∈ ↑s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i in s, w1 i = 1
hw1s : ↑(Finset.affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i in s, w2 i = 1
hw2s : ↑(Finset.affineCombination k s p) w2 = p i0
ha : Set.indicator (↑s) w2 = Set.indicator (↑s) w1
⊢ w2 i0 - w1 i0 = 0
rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]