awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i0 = 0
have hw1 : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i0 = 0
have hw1s : (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 ..
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i0 = 0
have hw2 : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i0 = 0
have hw2s : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i0 = 0
have ha₁ : (↑s : Set ι).indicator w2 = (↑s : Set ι).indicator w1
Tactic: replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
have 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
Tactic: rw [← Finset.mem_coe] at hi0
Cleared hypotheses: hi0, w1, hw1, hw1s, w2, hw2, hw2s, ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ w2 i0 - w1 i0 = 0
have rw : (↑s : Set ι).indicator w2 i0 - w1 i0 = 0
Tactic: rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ w2 i0 - w1 i0 = 0
have rw₁ : (↑s : Set ι).indicator w2 i0 - (↑s : Set ι).indicator w1 i0 = 0
Tactic: rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ w2 i0 - w1 i0 = 0
have rw₂ : (↑s : Set ι).indicator w1 i0 - (↑s : Set ι).indicator w1 i0 = 0
Tactic: rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ w2 i0 - w1 i0 = 0
have rw₃ : Eq.{u_1 + 1} (α := k) 0 0
Tactic: rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i0 = 0
have hws : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ 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
have 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
Tactic: classical
    constructor
    · intro ha s1 s2 w1 w2 hw1 hw2 heq
      ext i
      by_cases hi : i ∈ s1 ∪ s2
      · rw [← sub_eq_zero]
        rw [← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))] at hw1
        rw [← Finset.sum_indicator_subset w2 (s1.subset_union_right)] at hw2
        have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]
        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
        exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi
      · simp_all
    · intro ha s w hw hs i0 hi0
      let w1 : ι → k := Function.update (Function.const ι 0) i0 1
      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]
      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 ..
      let w2 := w + w1
      have hw2 : ∑ i ∈ s, w2 i = 1 := by
        simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]
      have hw2s : s.affineCombination k p w2 = p i0 := by
        simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
      replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
      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]
      simpa [w2] using hws
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ 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
have 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
Tactic: classical
    constructor
    · intro ha s1 s2 w1 w2 hw1 hw2 heq
      ext i
      by_cases hi : i ∈ s1 ∪ s2
      · rw [← sub_eq_zero]
        rw [← Finset.sum_indicator_subset w1 (s1.subset_union_left (s₂ := s2))] at hw1
        rw [← Finset.sum_indicator_subset w2 (s1.subset_union_right)] at hw2
        have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]
        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
        exact ha (s1 ∪ s2) (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) hws heq i hi
      · simp_all
    · intro ha s w hw hs i0 hi0
      let w1 : ι → k := Function.update (Function.const ι 0) i0 1
      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]
      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 ..
      let w2 := w + w1
      have hw2 : ∑ i ∈ s, w2 i = 1 := by
        simp_all only [w2, Pi.add_apply, Finset.sum_add_distrib, zero_add]
      have hw2s : s.affineCombination k p w2 = p i0 := by
        simp_all only [w2, ← Finset.weightedVSub_vadd_affineCombination, zero_vadd]
      replace ha := ha s s w2 w1 hw2 hw1 (hw1s.symm ▸ hw2s)
      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]
      simpa [w2] using hws
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ 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
have 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
Tactic: rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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)
⊢ (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
have hw1' : 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)]