-- 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
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
rw₇ rw₈ :
  ∀ (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),
    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₂))) (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),
    let w' := 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), False
rw₁₀ rw₁₁ :
  ∀ (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),
    let w' := 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'),
      False
rw₁₂ rw₁₃ :
  ∀ (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'), 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₂))) (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
        let w'' := (↑(map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs) : Set ι).indicator w';
        ∀ (hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''), False
rw₁₅ rw₁₆ :
  ∀ (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
        let w'' := (↑(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), 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₂))) (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
        let w'' := (↑(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) (hi : i ∈ fs'), 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₂))) (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
        let w'' := (↑(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) (hi : i ∈ fs') (hj : j ∈ fs'), 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₂))) (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
        let w'' := (↑(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),
          let w''' := w'' - weightedVSubVSubWeights k i j;
          ∀ (hi : i ∈ fs') (hj : j ∈ fs') (hw''' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0), 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₂))) (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),
    let w' := 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'),
      let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
      ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
        let w'' := (↑(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),
          let w''' := 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
⊢ 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₂))) (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),
  let w' := 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'),
    let fs' := insert i (insert j (map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs));
    ∀ (hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'),
      let w'' := (↑(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),
        let w''' := 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)) (h0 : w''' i = 0),
          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₁