awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : ι
s : Set ι
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i) ↔ i ∈ s
have mp : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i) → i ∈ 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
i : ι
s : Set ι
mp : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i) → i ∈ s
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i) ↔ i ∈ s
have mpr : i ∈ s → Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
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 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
⊢ i ∈ s
have h : ∃ (i_1 : ι), i_1 ∈ s ∩ {i}
Tactic: have h :=
      AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan ha hs
        (mem_affineSpan k (Set.mem_image_of_mem _ (Set.mem_singleton _)))
-- 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
i : ι
s : Set ι
hs : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
h : ∃ (i_1 : ι), i_1 ∈ s ∩ {i}
⊢ i ∈ s
have mp : ∀ (h : (s ∩ {i}).Nonempty), i ∈ s
Tactic: rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h
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
i : ι
s : Set ι
hs : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) (p i)
h : ∃ (i_1 : ι), i_1 ∈ s ∩ {i}
mp : ∀ (h : (s ∩ {i}).Nonempty), i ∈ s
⊢ i ∈ s
have mp₁ : ∀ (h : i ∈ s), i ∈ s
Tactic: rwa [← Set.nonempty_def, Set.inter_singleton_nonempty] at h
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
⊢ Injective.{u_4 + 1, u_3 + 1} (β := AffineSubspace k P) fun (s : Set ι) ↦ affineSpan k (p '' s)
have by_contra : ∀ (hn : ¬Injective.{u_4 + 1, u_3 + 1} (β := AffineSubspace k P) fun (s : Set ι) ↦ affineSpan k (p '' s)), False
Tactic: by_contra hn
-- 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
hn : ¬Injective.{u_4 + 1, u_3 + 1} (β := AffineSubspace k P) fun (s : Set ι) ↦ affineSpan k (p '' s)
⊢ False
have hn₁ : ∃ (a : Set ι) (b : Set ι), Eq (α := AffineSubspace k P) (affineSpan k (p '' a)) (affineSpan k (p '' b)) ∧ a ≠ b
Tactic: rw [not_injective_iff] at hn
Cleared hypotheses: hn
-- 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
hn : ∃ (a : Set ι) (b : Set ι), Eq (α := AffineSubspace k P) (affineSpan k (p '' a)) (affineSpan k (p '' b)) ∧ a ≠ b
⊢ False
have obtain : ∀ (s₁ s₂ : Set ι) (hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂)))
  (hne : s₁ ≠ s₂), False
Tactic: obtain ⟨s₁, s₂, hs₁₂, hne⟩ := hn
Cleared hypotheses: hn
-- 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 ι
hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂))
hne : s₁ ≠ s₂
⊢ False
have apply : s₁ = s₂
Tactic: apply hne
-- 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 ι
hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂))
hne : s₁ ≠ s₂
⊢ s₁ = s₂
have h : ∀ (i : ι), i ∈ s₁ ↔ i ∈ s₂
Tactic: ext i
-- 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 ι
hs₁₂ : Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁)) (affineSpan k (p '' s₂))
hne : s₁ ≠ s₂
i : ι
⊢ i ∈ s₁ ↔ i ∈ s₂
have h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁)) (p i) ↔
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₂)) (p i)
Tactic: simp_rw [← ha.mem_affineSpan_iff, 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
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 h₂ : s₁.Nontrivial
Tactic: rw [Set.not_subsingleton_iff] at h₁
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₁.Nontrivial
⊢ Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
have obtain : ∀ (j : ι) (hj : j ∈ s₁) (hne : j ≠ i), Ne (α := Submodule k V) (vectorSpan k (p '' s₁)) (vectorSpan k (p '' s₂))
Tactic: obtain ⟨j, hj, hne⟩ := h₁.exists_ne 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
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₂))
⊢ False
have hs : Membership.mem (γ := Submodule k V) (vectorSpan k (p '' s₁)) (p i -ᵥ p j)
Tactic: 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)
-- 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₂))
hs : Membership.mem (γ := Submodule k V) (vectorSpan k (p '' s₁)) (p i -ᵥ p j)
⊢ False
have 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
Tactic: rw [he, Set.image_eq_range, mem_vectorSpan_iff_eq_weightedVSub] at hs
Cleared hypotheses: 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
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₂))
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
have obtain : ∀ (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
Tactic: obtain ⟨fs, w, hw, hs⟩ := hs
Cleared hypotheses: 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
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
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
have simp : Eq.{u_1 + 1} (α := k) (∑ x ∈ fs, w' (↑x : ι)) (∑ i ∈ fs, w i)
Tactic: simp only [sum_map, Embedding.subtype_apply, ← hw]
-- 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
⊢ False
have hw' : Eq.{u_1 + 1} (α := k) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t) 0
Tactic: 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']
-- 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₁.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
⊢ p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
have rw : Eq.{u_2 + 1} (α := V)
  ((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 :
    V)
  ((fs.weightedVSub (p ∘ (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s₂) : (a : { x : ι // x ∈ s₂ }) → ι)) :
        (a : { x : ι // x ∈ s₂ } → k) → V)
      (w' ∘ (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s₂) : (a : { x : ι // x ∈ s₂ }) → ι)) :
    V)
Tactic: rw [hs, weightedVSub_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
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
⊢ False
have hs' : p i -ᵥ p j = ((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w'
Tactic: have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
-- 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))
⊢ False
have hfsfs' : map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'
Tactic: have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
-- 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₁.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'
⊢ p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
have rw : Eq.{u_2 + 1} (α := V) (((map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs).weightedVSub p : (a : ι → k) → V) w' : V)
  ((fs'.weightedVSub p : (a : ι → k) → V) w'' : V)
Tactic: rw [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
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'
⊢ False
have hs'' : p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''
Tactic: have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
-- 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₁.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''
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
have rw : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t)
Tactic: rw [← hw']
-- 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''
⊢ False
have hw'' : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0
Tactic: have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (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 : 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
⊢ False
have hi : i ∈ fs'
Tactic: have hi : i ∈ fs' := by grind