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
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
hws : w2 i0 - w1 i0 = 0
⊢ w i0 = 0

Tactic:
simpa [w2] using hws
-- 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
inst_4 : Fintype ι
p : ι → P
rw :
  (∀ (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) ↔
    ∀ (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
              ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
            w1 = w2
⊢ AffineIndependent k p ↔
    ∀ (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
              ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
            w1 = w2

Tactic:
rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq]

Premises used: affineIndependent_iff_indicator_eq_of_affineCombination_eq
-- 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
inst_4 : Fintype ι
p : ι → P
mp :
  (∀ (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) →
    ∀ (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
              ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
            w1 = w2
mpr :
  (∀ (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
              ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
            w1 = w2) →
    ∀ (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
⊢ (∀ (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) ↔
    ∀ (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
              ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
            w1 = 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (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
w1 w2 : ι → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1
hw2 : Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
    ((affineCombination k univ p : (a : ι → k) → P) w2 : P)
⊢ w1 = w2

Tactic:
simpa only [Set.indicator_univ, Finset.coe_univ] using h _ _ w1 w2 hw1 hw2 hweq

Premises used: Finset.coe_univ, Set.indicator_univ
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
rwa rwa₁ rwa₂ rwa₃ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1

Tactic:
rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s1)]

Premises used: Finset.sum_indicator_subset, Finset.subset_univ
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1

Tactic:
have hw1' : (∑ i, (s1 : Set ι).indicator w1 i) = 1 := by
      rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s1)]
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
rwa rwa₁ rwa₂ rwa₃ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1

Tactic:
rwa [Finset.sum_indicator_subset _ (Finset.subset_univ s2)]

Premises used: Finset.sum_indicator_subset, Finset.subset_univ
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1

Tactic:
have hw2' : (∑ i, (s2 : Set ι).indicator w2 i) = 1 := by
      rwa [Finset.sum_indicator_subset _ (Finset.subset_univ 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
hw2' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) ((↑s1 : Set ι).indicator w1) : P)
    ((affineCombination k univ p : (a : ι → k) → P) ((↑s2 : Set ι).indicator w2) : P)

Tactic:
rw [Finset.affineCombination_indicator_subset w1 p (Finset.subset_univ s1),
      Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq

Premises used: Finset.affineCombination_indicator_subset, Finset.subset_univ
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
hw2' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1
hweq₁ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) ((↑s1 : Set ι).indicator w1) : P)
    ((affineCombination k univ p : (a : ι → k) → P) ((↑s2 : Set ι).indicator w2) : P)
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1

Tactic:
rw [Finset.affineCombination_indicator_subset w1 p (Finset.subset_univ s1),
      Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq

Premises used: Finset.affineCombination_indicator_subset, Finset.subset_univ
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
    ((affineCombination k s2 p : (a : ι → k) → P) w2 : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
hw2' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1
hweq₁ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) ((↑s1 : Set ι).indicator w1) : P)
    ((affineCombination k univ p : (a : ι → k) → P) ((↑s2 : Set ι).indicator w2) : P)
hw1'₁ : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1

Tactic:
rw [Finset.affineCombination_indicator_subset w1 p (Finset.subset_univ s1),
      Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq

Premises used: Finset.affineCombination_indicator_subset, Finset.subset_univ
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) ((↑s1 : Set ι).indicator w1) : P)
    ((affineCombination k univ p : (a : ι → k) → P) ((↑s2 : Set ι).indicator w2) : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
hw2' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1
⊢ (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2

Tactic:
h _ _ hw1' hw2' hweq
-- 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
inst_4 : Fintype ι
p : ι → P
h :
  ∀ (w1 w2 : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w1 i) 1 →
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w2 i) 1 →
        Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) w1 : P)
            ((affineCombination k univ p : (a : ι → k) → P) w2 : P) →
          w1 = w2
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
hweq :
  Eq.{u_3 + 1} (α := P) ((affineCombination k univ p : (a : ι → k) → P) ((↑s1 : Set ι).indicator w1) : P)
    ((affineCombination k univ p : (a : ι → k) → P) ((↑s2 : Set ι).indicator w2) : P)
hw1' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s1 : Set ι).indicator w1 i) 1
hw2' : Eq.{u_1 + 1} (α := k) (∑ i : ι, (↑s2 : Set ι).indicator w2 i) 1
⊢ (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2

Tactic:
exact h _ _ hw1' hw2' hweq
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
v : ι → V
hv : LinearIndependent k v
s : Finset ι
w : ι → k
hw0 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hwv : Eq.{u_2 + 1} (α := V) ((s.weightedVSub v : (a : ι → k) → V) w : V) (0 : V)
i : ι
hi : i ∈ s
rw : ∀ (hwv : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (v i -ᵥ 0)) 0) (i : ι) (hi : i ∈ s), w i = 0
⊢ w i = 0

Tactic:
rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ hw0 0,
    Finset.weightedVSubOfPoint_apply] at hwv

Premises used: Finset.weightedVSubOfPoint_apply, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
v : ι → V
hv : LinearIndependent k v
s : Finset ι
w : ι → k
hw0 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hwv : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (v i -ᵥ 0)) 0
i : ι
hi : i ∈ s
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • v x) 0

Tactic:
simp only [vsub_eq_sub, sub_zero] at hwv

Premises used: sub_zero, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
v : ι → V
hv : LinearIndependent k v
s : Finset ι
w : ι → k
hw0 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
i : ι
hi : i ∈ s
hwv : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • v x) 0
⊢ w i = 0

Tactic:
linearIndependent_iff'.mp hv s w hwv i hi

Premises used: linearIndependent_iff', Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
v : ι → V
hv : LinearIndependent k v
s : Finset ι
w : ι → k
hw0 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
i : ι
hi : i ∈ s
hwv : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • v x) 0
⊢ w i = 0

Tactic:
exact linearIndependent_iff'.mp hv s w hwv i hi

Premises used: linearIndependent_iff', Iff.mp
-- 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
hp : AffineIndependent k p
j : ι
w : ι → kˣ
rw :
  ∀ (hp : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j) (w : ι → kˣ),
    LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦
      VSub.vsub.{u_2, u_3} (P := P) ((AffineMap.lineMap (p j) (p (↑i : ι)) : (a : k) → P) (↑(w (↑i : ι)) : k) : P)
        ((AffineMap.lineMap (p j) (p j) : (a : k) → P) (↑(w j) : k) : P)
⊢ AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (i : ι) ↦
    (AffineMap.lineMap (p j) (p i) : (a : k) → P) (↑(w i) : k)

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k _ j] at hp ⊢

Premises used: affineIndependent_iff_linearIndependent_vsub
-- 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
j : ι
hp : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
w : ι → kˣ
simp :
  LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ (↑(w (↑i : ι)) : k) • (p (↑i : ι) -ᵥ p j)
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦
    VSub.vsub.{u_2, u_3} (P := P) ((AffineMap.lineMap (p j) (p (↑i : ι)) : (a : k) → P) (↑(w (↑i : ι)) : k) : P)
      ((AffineMap.lineMap (p j) (p j) : (a : k) → P) (↑(w j) : k) : P)

Tactic:
simp only [AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same, const_apply]

Premises used: Function.const_apply, AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same
-- 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
j : ι
hp : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ (↑(w (↑i : ι)) : k) • (p (↑i : ι) -ᵥ p j)

Tactic:
hp.units_smul fun i => w i

Premises used: LinearIndependent.units_smul, Subtype.val
-- 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
j : ι
hp : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ (↑(w (↑i : ι)) : k) • (p (↑i : ι) -ᵥ p j)

Tactic:
exact hp.units_smul fun i => w i

Premises used: LinearIndependent.units_smul, Subtype.val
-- 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
s₁ s₂ : Finset ι
w₁ w₂ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k s₂ p : (a : ι → k) → P) w₂ : P)
⊢ (↑s₁ : Set ι).indicator w₁ = (↑s₂ : Set ι).indicator w₂

Tactic:
(affineIndependent_iff_indicator_eq_of_affineCombination_eq k p).1 ha s₁ s₂ w₁ w₂ hw₁ hw₂ h

Premises used: affineIndependent_iff_indicator_eq_of_affineCombination_eq, Iff.mp
-- 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
w₁ w₂ : ι → k
s : Finset ι
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) ↔
    ∀ i ∈ s, w₁ i = w₂ i

Tactic:
⟨fun h ↦ ?_, fun h ↦ s.affineCombination_congr h fun _ _ ↦ rfl⟩

Premises used: Finset.affineCombination_congr, Iff.intro, rfl
-- 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
w₁ w₂ : ι → k
s : Finset ι
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
refine :
  ∀
    (h :
      Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        ((affineCombination k s p : (a : ι → k) → P) w₂ : P)),
    ∀ i ∈ s, w₁ i = w₂ i
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) ↔
    ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ s.affineCombination_congr h fun _ _ ↦ rfl⟩
-- 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
w₁ w₂ : ι → k
s : Finset ι
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
⊢ (↑s : Set ι).indicator w₁ = (↑s : Set ι).indicator w₂

Tactic:
have hi := ha.indicator_eq_of_affineCombination_eq _ _ _ _ hw₁ hw₂ h