awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
mp :
  AffineIndependent k p →
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
              ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
            (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
mpr :
  (∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
              ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
            (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2) →
    AffineIndependent k p
⊢ AffineIndependent k p ↔
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
              ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
            (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
mp : ∀ (i : ι), (↑s1 : Set ι).indicator w1 i = (↑s2 : Set ι).indicator w2 i
⊢ (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
pos : ∀ (hi : i ∈ s1 ∪ s2), (↑s1 : Set ι).indicator w1 i = (↑s2 : Set ι).indicator w2 i
neg : ∀ (hi : i ∉ s1 ∪ s2), (↑s1 : Set ι).indicator w1 i = (↑s2 : Set ι).indicator w2 i
⊢ (↑s1 : Set ι).indicator w1 i = (↑s2 : Set ι).indicator w2 i

Tactic:
by_cases hi : i ∈ s1 ∪ s2
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∈ s1 ∪ s2
pos : (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0
⊢ (↑s1 : Set ι).indicator w1 i = (↑s2 : Set ι).indicator w2 i

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∈ s1 ∪ s2
pos :
  ∀ (hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1)
    (hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1)
    (heq :
      Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
        ((affineCombination k s2 p : (a : ι → k) → P) w2 : P))
    (i : ι) (hi : i ∈ s1 ∪ s2), (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0
⊢ (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0

Tactic:
rw [← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))] at hw1

Premises used: Finset.subset_union_left, Finset.sum_indicator_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∈ s1 ∪ s2
pos :
  ∀ (hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s2 : Set ι).indicator w2 i) 1)
    (heq :
      Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
        ((affineCombination k s2 p : (a : ι → k) → P) w2 : P))
    (i : ι) (hi : i ∈ s1 ∪ s2), (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0
⊢ (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0

Tactic:
rw [← Finset.sum_indicator_subset w2 (s1.subset_union_right)] at hw2

Premises used: Finset.sum_indicator_subset, Finset.subset_union_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s2 : Set ι).indicator w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∈ s1 ∪ s2
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) i) 0

Tactic:
simp [hw1, hw2]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s2 : Set ι).indicator w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∈ s1 ∪ s2
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) i) 0

Tactic:
have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s2 : Set ι).indicator w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∈ s1 ∪ s2
hws : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) i) 0
pos :
  ∀
    (heq :
      Eq.{u_2 + 1} (α := V)
        (((s1 ∪ s2).weightedVSub p : (a : ι → k) → V) ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) : V)
        (0 : V))
    (i : ι) (hi : i ∈ s1 ∪ s2)
    (hws : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) i) 0),
    (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0
⊢ (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0

Tactic:
rw [Finset.affineCombination_indicator_subset w1 p (s1.subset_union_left (s₂ := s2)),
          Finset.affineCombination_indicator_subset w2 p s1.subset_union_right,
          ← @vsub_eq_zero_iff_eq V, Finset.affineCombination_vsub] at heq

Premises used: Finset.affineCombination_vsub, vsub_eq_zero_iff_eq, Finset.subset_union_left, Finset.affineCombination_indicator_subset, Finset.subset_union_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s2 : Set ι).indicator w2 i) 1
heq :
  Eq.{u_2 + 1} (α := V)
    (((s1 ∪ s2).weightedVSub p : (a : ι → k) → V) ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) : V) (0 : V)
i : ι
hi : i ∈ s1 ∪ s2
hws : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) i) 0
⊢ (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0

Tactic:
ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi

Premises used: Set.indicator, HSub.hSub, Union.union
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s1 : Set ι).indicator w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, (↑s2 : Set ι).indicator w2 i) 1
heq :
  Eq.{u_2 + 1} (α := V)
    (((s1 ∪ s2).weightedVSub p : (a : ι → k) → V) ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) : V) (0 : V)
i : ι
hi : i ∈ s1 ∪ s2
hws : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1 ∪ s2, ((↑s1 : Set ι).indicator w1 - (↑s2 : Set ι).indicator w2) i) 0
⊢ (↑s1 : Set ι).indicator w1 i - (↑s2 : Set ι).indicator w2 i = 0

Tactic:
exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi

Premises used: Set.indicator, HSub.hSub, Union.union
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
heq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
i : ι
hi : i ∉ s1 ∪ s2
⊢ (↑s1 : Set ι).indicator w1 i = (↑s2 : Set ι).indicator w2 i

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
rw : HAdd.hAdd (α := k) 1 (∑ x ∈ s \ {i0}, const ι 0 x) = 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1

Tactic:
rw [Finset.sum_update_of_mem hi0]

Premises used: Finset.sum_update_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
⊢ HAdd.hAdd (α := k) 1 (∑ x ∈ s \ {i0}, const ι 0 x) = 1

Tactic:
simp only [Finset.sum_const_zero, add_zero, const_apply]

Premises used: Function.const_apply, Finset.sum_const_zero, add_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1

Tactic:
have hw1 : ∑ i ∈ s, w1 i = 1 := by
        rw [Finset.sum_update_of_mem hi0]
        simp only [Finset.sum_const_zero, add_zero, const_apply]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
⊢ (affineCombination k s p : (a : ι → k) → P) w1 = p i0

Tactic:
have hw1s : s.affineCombination k p w1 = p i0 :=
        s.affineCombination_of_eq_one_of_eq_zero w1 p hi0 (Function.update_self ..)
          fun _ _ hne => Function.update_of_ne hne ..
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1

Tactic:
simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]

Premises used: Finset.sum_add_distrib, zero_add, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1

Tactic:
have hw2 : ∑ i ∈ s, w2 i = 1 := by
        simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1
⊢ (affineCombination k s p : (a : ι → k) → P) w2 = p i0

Tactic:
simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]

Premises used: zero_vadd, Finset.weightedVSub_vadd_affineCombination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1
⊢ (affineCombination k s p : (a : ι → k) → P) w2 = p i0

Tactic:
have hw2s : s.affineCombination k p w2 = p i0 := by
        simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha :
  ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
            ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
          (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1
hw2s : (affineCombination k s p : (a : ι → k) → P) w2 = p i0
⊢ (↑s : Set ι).indicator w2 = (↑s : Set ι).indicator w1

Tactic:
replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1
hw2s : (affineCombination k s p : (a : ι → k) → P) w2 = p i0
ha : (↑s : Set ι).indicator w2 = (↑s : Set ι).indicator w1
rw :
  ∀ (hi0 : i0 ∈ (↑s : Set ι)),
    let w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1;
    ∀ (hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1) (hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0),
      let w2 := w + w1;
      ∀ (hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1) (hw2s : (affineCombination k s p : (a : ι → k) → P) w2 = p i0)
        (ha : (↑s : Set ι).indicator w2 = (↑s : Set ι).indicator w1), w2 i0 - w1 i0 = 0
⊢ w2 i0 - w1 i0 = 0

Tactic:
rw [← Finset.mem_coe] at hi0

Premises used: Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ (↑s : Set ι)
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1
hw2s : (affineCombination k s p : (a : ι → k) → P) w2 = p i0
ha : (↑s : Set ι).indicator w2 = (↑s : Set ι).indicator w1
rw : (↑s : Set ι).indicator w2 i0 - w1 i0 = 0
rw₁ : (↑s : Set ι).indicator w2 i0 - (↑s : Set ι).indicator w1 i0 = 0
rw₂ : (↑s : Set ι).indicator w1 i0 - (↑s : Set ι).indicator w1 i0 = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := k) 0 0
⊢ w2 i0 - w1 i0 = 0

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

Premises used: sub_self, Set.indicator_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (β := fun (a : ι) ↦ k) (const ι 0) i0 1
hw1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (affineCombination k s p : (a : ι → k) → P) w1 = p i0
w2 : ι → k := w + w1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w2 i) 1
hw2s : (affineCombination k s p : (a : ι → k) → P) w2 = p i0
ha : (↑s : Set ι).indicator w2 = (↑s : Set ι).indicator w1
⊢ w2 i0 - w1 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]