awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ 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:
simp [w', Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'

Tactic:
have hs' : p i -ᵥ p j = (fs.map (Embedding.subtype _)).weightedVSub p w' := by
    rw [hs, weightedVSub_map]
    simp [w', Function.comp_def]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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))
⊢ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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))
⊢ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'

Tactic:
have hfsfs' : fs.map (Embedding.subtype _) ⊆ fs' := by grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'
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)
⊢ p i -ᵥ p j = (fs'.weightedVSub p : (a : ι → k) → V) w''

Tactic:
rw [hs']
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'
⊢ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'
⊢ 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:
exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)

Premises used: Finset.weightedVSubOfPoint_indicator_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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''

Tactic:
have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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''
rw : Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t)
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w'' t) 0

Tactic:
rw [← hw']
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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''
⊢ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs ⊆ fs'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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) (∑ t ∈ map (Embedding.subtype fun (x : ι) ↦ x ∈ s₂) fs, w' t)

Tactic:
exact sum_indicator_subset _ (by grind)

Premises used: Finset.sum_indicator_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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

Tactic:
have hw'' : ∑ t ∈ fs', w'' t = 0 := by
    rw [← hw']
    exact sum_indicator_subset _ (by grind)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ i ∈ fs'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
⊢ i ∈ fs'

Tactic:
have hi : i ∈ fs' := by grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'
⊢ j ∈ fs'

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'
⊢ j ∈ fs'

Tactic:
have hj : j ∈ fs' := by grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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'
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ fs', w''' t) 0

Tactic:
simp [w''', sum_sub_distrib, hw'', hi, hj]

Premises used: Finset.sum_sub_distrib