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
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
⊢ (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2
have hw2' : 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)]
-- 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)
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
have 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)
Tactic: rw [Finset.affineCombination_indicator_subset w1 p (Finset.subset_univ s1),
      Finset.affineCombination_indicator_subset w2 p (Finset.subset_univ s2)] at hweq
Cleared hypotheses: hweq, hw1', hw2'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ w i = 0
have rw : ∀ (hwv : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (v i -ᵥ 0)) 0) (i : ι) (hi : i ∈ s), w i = 0
Tactic: rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ hw0 0,
    Finset.weightedVSubOfPoint_apply] at hwv
Cleared hypotheses: hwv, i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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
⊢ w i = 0
have hwv₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • v x) 0
Tactic: simp only [vsub_eq_sub, sub_zero] at hwv
Cleared hypotheses: hwv
-- 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
hp : AffineIndependent k p
j : ι
w : ι → kˣ
⊢ 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)
have 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)
Tactic: rw [affineIndependent_iff_linearIndependent_vsub k _ j] at hp ⊢
Cleared hypotheses: hp, w
-- 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
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 }) ↦
    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)
have simp : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ (↑(w (↑i : ι)) : k) • (p (↑i : ι) -ᵥ p j)
Tactic: simp only [AffineMap.lineMap_vsub_left, AffineMap.coe_const, AffineMap.lineMap_same, const_apply]
-- 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
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ s.affineCombination_congr h fun _ _ ↦ rfl⟩
-- 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 : 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)
⊢ ∀ i ∈ s, w₁ i = w₂ i
have hi : (↑s : Set ι).indicator w₁ = (↑s : Set ι).indicator w₂
Tactic: have hi := ha.indicator_eq_of_affineCombination_eq _ _ _ _ hw₁ hw₂ h
-- 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
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)
hi : (↑s : Set ι).indicator w₁ = (↑s : Set ι).indicator w₂
i : ι
hs : i ∈ s
⊢ w₁ i = w₂ i
have suffices : (↑s : Set ι).indicator w₁ i = (↑s : Set ι).indicator w₂ i
Tactic: suffices Set.indicator s w₁ i = Set.indicator s w₂ i by simpa [hs] using this
-- 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 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i j : ι
hij : p i = p j
⊢ i = j
have ha₁ : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
Tactic: rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha
Cleared hypotheses: ha, hij
-- 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 : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
hij : p i = p j
⊢ i = j
have by_contra : ∀ (hij' : ¬i = j), False
Tactic: by_contra hij'
-- 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 : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ j }) ↦ p (↑i : ι) -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ False
have refine : p (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ j) i hij') : ι) = p j
Tactic: refine ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
i2 : ι2
⊢ w' ((f : (a : ι2) → ι) i2) = w i2
have h : ∃ (i : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)
Tactic: have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
i2 : ι2
h : ∃ (i : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)
⊢ w' ((f : (a : ι2) → ι) i2) = w i2
have hs₁ : h.choose (p := fun (i : ι2) ↦ Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)) = i2
Tactic: have hs : h.choose = i2 := f.injective h.choose_spec
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs_1 : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
i2 : ι2
h : ∃ (i : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)
hs : h.choose (p := fun (i : ι2) ↦ Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i : ι) ((f : (a : ι2) → ι) i2 : ι)) = i2
simp_rw :
  (if h : ∃ (i2_1 : ι2), Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i2_1 : ι) ((f : (a : ι2) → ι) i2 : ι) then
      w
        (h.choose (p := fun (i2_1 : ι2) ↦
          Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i2_1 : ι) ((f : (a : ι2) → ι) i2 : ι)))
    else 0) =
    w i2
⊢ w' ((f : (a : ι2) → ι) i2) = w i2
have simp_rw₁ : w (h.choose (p := fun (i2_1 : ι2) ↦ Eq.{u_4 + 1} (α := ι) ((f : (a : ι2) → ι) i2_1 : ι) ((f : (a : ι2) → ι) i2 : ι))) =
  w i2
Tactic: simp_rw [w', dif_pos h, hs]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
⊢ w i0 = 0
have hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
Tactic: have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
have rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ fs, w' ((f : (a : ι2) → ι) x)) (∑ i ∈ fs, w i)
Tactic: rw [← hw, Finset.sum_map]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
⊢ w i0 = 0
have hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
Tactic: have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
⊢ Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)
have rw : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) (w' ∘ (⇑f : (a : ι2) → ι)) : V)
  ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V)
Tactic: rw [← hs, Finset.weightedVSub_map]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
⊢ Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) (w' ∘ (⇑f : (a : ι2) → ι)) : V)
    ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V)
have h : ∀ (i : ι2), (w' ∘ (⇑f : (a : ι2) → ι)) i = w i
Tactic: congr with i
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
⊢ w i0 = 0
have hs' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)
Tactic: have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
hs' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)
⊢ w i0 = 0
have rw : w i0 = w' ((f : (a : ι2) → ι) i0)
Tactic: rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : (i : ι) → k :=
  fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0
hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2
hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0
hs' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w' : V) (0 : V)
rw : w i0 = w' ((f : (a : ι2) → ι) i0)
⊢ w i0 = 0
have rw₁ : w i0 = w i0
Tactic: rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
⊢ AffineIndependent.{u_1, u_2, u_3, u_5} k (ι := ι2) (p ∘ (⇑f : (a : ι2) → ι))
have intro : ∀ (fs : Finset ι2) (w : ι2 → k),
  Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0 →
    Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V) →
      ∀ i ∈ fs, w i = 0
Tactic: classical
    intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
intro intro₁ intro₂ intro₃ intro₄ intro₅ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₆ intro₇ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
⊢ AffineIndependent.{u_1, u_2, u_3, u_5} k (ι := ι2) (p ∘ (⇑f : (a : ι2) → ι))
have intro₈ : ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
  (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)) (i0 : ι2)
  (hi0 : i0 ∈ fs),
  let w' : (i : ι) → k := fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0;
  ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2), w i0 = 0
Tactic: classical
    intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']