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 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
⊢ False
have hj₁ : j ∈ fs'
Tactic: have hj : j ∈ fs' := by grind
-- 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
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
⊢ False
have hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
Tactic: have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
-- 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
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
⊢ False
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 := by
    simp [w''', ← hs'', hi, hj]
-- 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
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj_1 : j ∈ s₁
hne : j ≠ i
he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
fs : Finset (↑s₂ : Type u_4)
w : (↑s₂ : Type u_4) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0
hs :
  p i -ᵥ p j =
    (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
        (a : (↑s₂ : Type u_4) → k) → V)
      w
w' : ι → k := extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s₂)) w 0
hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
w''' : ι → k := w'' - weightedVSubVSubWeights k i j
hi : i ∈ fs'
hj : j ∈ fs'
hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0
hs''' : Eq.{u_2 + 1} (α := V) ((fs'.weightedVSub p : (a : ι → k) → V) w''' : V) (0 : V)
⊢ False
have h0 : w''' i = 0
Tactic: have h0 := ha fs' w''' hw''' hs''' i hi
-- 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
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : ¬s₁.Subsingleton
⊢ Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
have rw : ∀ (h₁ : s₁.Nontrivial), Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
Tactic: classical
  rw [Set.not_subsingleton_iff] at h₁
  obtain ⟨j, hj, hne⟩ := h₁.exists_ne i
  intro he
  have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ hj)
  rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs
  obtain ⟨fs, w, hw, hs⟩ := hs
  let w' : ι → k := Function.extend Subtype.val w 0
  have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']
  have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
  let fs' : Finset ι := insert i (insert j (fs.map (Embedding.subtype _)))
  have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
  let w'' : ι → k := Set.indicator (fs.map (Embedding.subtype _)) w'
  have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
  have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (by grind)
  let w''' : ι → k := w'' - weightedVSubVSubWeights k i j
  have hi : i ∈ fs' := by grind
  have hj : j ∈ fs' := by grind
  have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
  have hs''' : fs'.weightedVSub p w''' = 0 := by
    simp [w''', ← hs'', hi, hj]
  have h0 := ha fs' w''' hw''' hs''' i hi
  simp [w''', w'', Pi.sub_apply, hne.symm, his₂] at h0
Cleared hypotheses: 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
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : ¬s₁.Subsingleton
rw rw₁ rw₂ : ∀ (h₁ : s₁.Nontrivial), Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
⊢ Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
have rw₃ : ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i),
  Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
Tactic: classical
  rw [Set.not_subsingleton_iff] at h₁
  obtain ⟨j, hj, hne⟩ := h₁.exists_ne i
  intro he
  have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ hj)
  rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs
  obtain ⟨fs, w, hw, hs⟩ := hs
  let w' : ι → k := Function.extend Subtype.val w 0
  have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']
  have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
  let fs' : Finset ι := insert i (insert j (fs.map (Embedding.subtype _)))
  have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
  let w'' : ι → k := Set.indicator (fs.map (Embedding.subtype _)) w'
  have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
  have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (by grind)
  let w''' : ι → k := w'' - weightedVSubVSubWeights k i j
  have hi : i ∈ fs' := by grind
  have hj : j ∈ fs' := by grind
  have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
  have hs''' : fs'.weightedVSub p w''' = 0 := by
    simp [w''', ← hs'', hi, hj]
  have h0 := ha fs' w''' hw''' hs''' i hi
  simp [w''', w'', Pi.sub_apply, hne.symm, his₂] at h0
Cleared hypotheses: 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
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : ¬s₁.Subsingleton
rw rw₁ rw₂ : ∀ (h₁ : s₁.Nontrivial), Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
rw₃ :
  ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i),
    Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
rw₄ :
  ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i)
    (he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))), False
⊢ Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
have rw₅ : ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i)
  (he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)))
  (hs : Membership.mem (γ := Submodule k V) (vectorSpan k (p '' s₁)) (p i -ᵥ p j)), False
Tactic: classical
  rw [Set.not_subsingleton_iff] at h₁
  obtain ⟨j, hj, hne⟩ := h₁.exists_ne i
  intro he
  have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ hj)
  rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs
  obtain ⟨fs, w, hw, hs⟩ := hs
  let w' : ι → k := Function.extend Subtype.val w 0
  have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']
  have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
  let fs' : Finset ι := insert i (insert j (fs.map (Embedding.subtype _)))
  have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
  let w'' : ι → k := Set.indicator (fs.map (Embedding.subtype _)) w'
  have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
  have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (by grind)
  let w''' : ι → k := w'' - weightedVSubVSubWeights k i j
  have hi : i ∈ fs' := by grind
  have hj : j ∈ fs' := by grind
  have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
  have hs''' : fs'.weightedVSub p w''' = 0 := by
    simp [w''', ← hs'', hi, hj]
  have h0 := ha fs' w''' hw''' hs''' i hi
  simp [w''', w'', Pi.sub_apply, hne.symm, his₂] at h0
Cleared hypotheses: 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
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : ¬s₁.Subsingleton
rw rw₁ rw₂ : ∀ (h₁ : s₁.Nontrivial), Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
rw₃ :
  ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i),
    Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
rw₄ :
  ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i)
    (he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))), False
rw₅ :
  ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i)
    (he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)))
    (hs : Membership.mem (γ := Submodule k V) (vectorSpan k (p '' s₁)) (p i -ᵥ p j)), False
⊢ Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
have rw₆ : ∀ (h₁ : s₁.Nontrivial) (j : ι) (hj : j ∈ s₁) (hne : j ≠ i)
  (he : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)))
  (hs :
    ∃ (s : Finset (↑s₂ : Type u_4)) (w : (↑s₂ : Type u_4) → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧
        p i -ᵥ p j =
          (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : (↑s₂ : Type u_4)) ↦ p (↑x : ι) :
              (a : (↑s₂ : Type u_4) → k) → V)
            w),
  False
Tactic: classical
  rw [Set.not_subsingleton_iff] at h₁
  obtain ⟨j, hj, hne⟩ := h₁.exists_ne i
  intro he
  have hs : p i -ᵥ p j ∈ vectorSpan k (p '' s₁) :=
    vsub_mem_vectorSpan k (Set.mem_image_of_mem _ his₁) (Set.mem_image_of_mem _ hj)
  rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs
  obtain ⟨fs, w, hw, hs⟩ := hs
  let w' : ι → k := Function.extend Subtype.val w 0
  have hw' : ∑ t ∈ fs.map (Embedding.subtype _), w' t = 0 := by
    simp only [sum_map, Embedding.subtype_apply, ← hw]
    exact sum_congr rfl fun t ht ↦ by simp [w']
  have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
  let fs' : Finset ι := insert i (insert j (fs.map (Embedding.subtype _)))
  have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
  let w'' : ι → k := Set.indicator (fs.map (Embedding.subtype _)) w'
  have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
  have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (by grind)
  let w''' : ι → k := w'' - weightedVSubVSubWeights k i j
  have hi : i ∈ fs' := by grind
  have hj : j ∈ fs' := by grind
  have hw''' : ∑ t ∈ fs', w''' t = 0 := by
    simp [w''', sum_sub_distrib, hw'', hi, hj]
  have hs''' : fs'.weightedVSub p w''' = 0 := by
    simp [w''', ← hs'', hi, hj]
  have h0 := ha fs' w''' hw''' hs''' i hi
  simp [w''', w'', Pi.sub_apply, hne.symm, his₂] at h0
Cleared hypotheses: 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
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)) ↔
    s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
have mp : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)) → s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
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 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
mp :
  Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)) →
    s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂)) ↔
    s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
have mpr : s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton → Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
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 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
have pos : ∀ (he : s₁ = s₂), s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: by_cases he : s₁ = s₂
-- 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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
pos : ∀ (he : s₁ = s₂), s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
have neg : ∀ (he : ¬s₁ = s₂), s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: by_cases he : s₁ = s₂
-- 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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
⊢ s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton
have neg : s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: simp only [he, false_or]
-- 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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have pos : ∀ (h₁ : s₁.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: by_cases h₁ : s₁.Subsingleton
-- 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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
pos : ∀ (h₁ : s₁.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have neg : ∀ (h₁ : ¬s₁.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: by_cases h₁ : s₁.Subsingleton
-- 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
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have h₂ : (p '' s₂).Subsingleton
Tactic: rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h
Cleared hypotheses: h, he, 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
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have pos : ∀ (h₂ : s₂.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: by_cases h₂ : s₂.Subsingleton
-- 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
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
pos : ∀ (h₂ : s₂.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have neg : ∀ (h₂ : ¬s₂.Subsingleton), s₁.Subsingleton ∧ s₂.Subsingleton
Tactic: by_cases h₂ : s₂.Subsingleton
-- 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
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have h₃ : (p '' s₁).Subsingleton
Tactic: rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h
Cleared hypotheses: h, he, h₁, 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
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
⊢ s₁.Subsingleton ∧ s₂.Subsingleton
have neg : False
Tactic: simp only [h₁, h₂, false_and]
-- 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
s₁ s₂ : Set ι
h : Eq (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
he : ¬s₁ = s₂
h₁ : ¬s₁.Subsingleton
h₂ : ¬s₂.Subsingleton
⊢ False
have hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁
Tactic: have hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁ := by grind