-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq (p : ι → P) :
    AffineIndependent k p ↔
      ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
        ∑ i ∈ s1, w1 i = 1 →
          ∑ i ∈ s2, w2 i = 1 →
            s1.affineCombination k p w1 = s2.affineCombination k p w2 →
              Set.indicator (↑s1) w1 = Set.indicator (↑s2) w2

Proof state:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ ∑ i ∈ s, w1 i = 1

Tactic:
rw [Finset.sum_update_of_mem hi0]

Result:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ 1 + ∑ x ∈ s \ {i0}, const ι 0 x = 1

Proof state:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
⊢ w i0 = 0

Tactic:
replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)

Result:
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 ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w i0 = 0

Proof state:
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 ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w i0 = 0

Tactic:
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]

Result:
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 ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
hws : w2 i0 - w1 i0 = 0
⊢ w i0 = 0

Proof state:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
⊢ w i0 = 0

Tactic:
let w2 := w + w1

Result:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
⊢ w i0 = 0

Proof state:
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 ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ ↑s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w2 i0 - w1 i0 = 0

Tactic:
rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]

Result:
no goals

Proof state:
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 ∈ s1, w1 i = 1 →
        ∑ i ∈ s2, w2 i = 1 →
          (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2) →
    AffineIndependent k p

Tactic:
intro ha s w hw hs i0 hi0

Result:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
⊢ w i0 = 0

Proof state:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
⊢ w i0 = 0

Tactic:
let w1 : ι → k := Function.update (Function.const ι 0) i0 1

Result:
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 ∈ s1, w1 i = 1 →
      ∑ i ∈ s2, w2 i = 1 →
        (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
⊢ w i0 = 0