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 : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)

Tactic:
have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0

Tactic:
simp [wm, ← Finset.mul_sum, hw]

Premises used: Finset.mul_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0

Tactic:
have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
⊢ wm i = -1

Tactic:
simp [wm, his.2]

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
⊢ wm i = -1

Tactic:
have hwmi : wm i = -1 := by simp [wm, his.2]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s with x ≠ i, wm x) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 1

Tactic:
simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]

Premises used: Finset.sum_subtype_eq_sum_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
⊢ HAdd.hAdd (α := k) (∑ x ∈ s with x ≠ i, wm x) (∑ x ∈ s with ¬x ≠ i, wm x) = 0

Tactic:
rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm

Premises used: Ne, Finset.sum_filter_add_sum_filter_not
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
hwm₁ : HAdd.hAdd (α := k) (∑ x ∈ s with x ≠ i, wm x) (∑ x ∈ s with ¬x ≠ i, wm x) = 0
⊢ wm i = -1

Tactic:
rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm

Premises used: Ne, Finset.sum_filter_add_sum_filter_not
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : HAdd.hAdd (α := k) (∑ x ∈ s with x ≠ i, wm x) (∑ x ∈ s with ¬x ≠ i, wm x) = 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s with x ≠ i, wm x) 1

Tactic:
simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm

Premises used: add_neg_eq_zero, Classical.not_not, Finset.filter_eq', if_pos, Finset.sum_singleton, And.left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 1

Tactic:
have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 1
pos :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (Set.range (ι := { x : ι // Membership.mem (γ := Set ι) {x : ι | x ≠ i} x })
        (p ∘ Subtype.val (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {x : ι | x ≠ i} x))))
    ((affineCombination k (Finset.subtype (fun (x : ι) ↦ x ≠ i) s) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) :
          (a : { x : ι // x ≠ i } → k) → P)
        fun (i_1 : { x : ι // x ≠ i }) ↦ wm (↑i_1 : ι) :
      P)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' {x : ι | x ≠ i})) (p i)

Tactic:
rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]

Premises used: Set.range_comp, Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, Subtype.range_coe, And.left, Finset.affineCombination_subtype_eq_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (Set.range (ι := { x : ι // Membership.mem (γ := Set ι) {x : ι | x ≠ i} x })
        (p ∘ Subtype.val (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {x : ι | x ≠ i} x))))
    ((affineCombination k (Finset.subtype (fun (x : ι) ↦ x ≠ i) s) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) :
          (a : { x : ι // x ≠ i } → k) → P)
        fun (i_1 : { x : ι // x ≠ i }) ↦ wm (↑i_1 : ι) :
      P)

Tactic:
affineCombination_mem_affineSpan hw' p'

Premises used: Set.Mem, setOf, affineCombination_mem_affineSpan, Not, Multiset.filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)
hwm : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, wm i) 0
hwmi : wm i = -1
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ wm (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (Set.range (ι := { x : ι // Membership.mem (γ := Set ι) {x : ι | x ≠ i} x })
        (p ∘ Subtype.val (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {x : ι | x ≠ i} x))))
    ((affineCombination k (Finset.subtype (fun (x : ι) ↦ x ≠ i) s) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) :
          (a : { x : ι // x ≠ i } → k) → P)
        fun (i_1 : { x : ι // x ≠ i }) ↦ wm (↑i_1 : ι) :
      P)

Tactic:
exact affineCombination_mem_affineSpan hw' p'

Premises used: affineCombination_mem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : ¬(i ∈ s ∧ w i ≠ 0)
⊢ i ∉ s ∨ w i = 0

Tactic:
rw [not_and_or, Classical.not_not] at his

Premises used: Classical.not_not, not_and_or
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
simp_rw : Eq.{u_1 + 1} (α := k) (∑ x ∈ s with x ≠ i, w x) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0

Tactic:
simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]

Premises used: Finset.sum_subtype_eq_sum_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
rw : ∀ x ∈ s, w x ≠ 0 → x ≠ i
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s with x ≠ i, w x) 0

Tactic:
rw [Finset.sum_filter_of_ne, hw]

Premises used: Finset.sum_filter_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
hi : p x ∉ affineSpan k (p '' {x_1 : ι | x_1 ≠ x})
s' : Finset { y : ι // y ≠ x } := Finset.subtype (fun (x_1 : ι) ↦ x_1 ≠ x) s
p' : { y : ι // y ≠ x } → P := fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
his : x ∉ s ∨ w x = 0
w' : { y : ι // y ≠ x } → k := fun (x_1 : { y : ι // y ≠ x }) ↦ w (↑x_1 : ι)
⊢ False

Tactic:
hwx (his.neg_resolve_left hxs)

Premises used: Or.neg_resolve_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
hi : p x ∉ affineSpan k (p '' {x_1 : ι | x_1 ≠ x})
s' : Finset { y : ι // y ≠ x } := Finset.subtype (fun (x_1 : ι) ↦ x_1 ≠ x) s
p' : { y : ι // y ≠ x } → P := fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
his : x ∉ s ∨ w x = 0
w' : { y : ι // y ≠ x } → k := fun (x_1 : { y : ι // y ≠ x }) ↦ w (↑x_1 : ι)
⊢ False

Tactic:
exact hwx (his.neg_resolve_left hxs)

Premises used: Or.neg_resolve_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
⊢ Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0

Tactic:
have hw' : ∑ x ∈ s', w' x = 0 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [Finset.sum_filter_of_ne, hw]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
simp_rw : Eq.{u_2 + 1} (α := V) (({x ∈ s | x ≠ i}.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
⊢ Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)

Tactic:
simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]

Premises used: Finset.weightedVSub_subtype_eq_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
h : ∀ i_1 ∈ s, w i_1 ≠ 0 → i_1 ≠ i
⊢ Eq.{u_2 + 1} (α := V) (({x ∈ s | x ≠ i}.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)

Tactic:
rw [Finset.weightedVSub_filter_of_ne, hs]

Premises used: Finset.weightedVSub_filter_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
hi : p x ∉ affineSpan k (p '' {x_1 : ι | x_1 ≠ x})
s' : Finset { y : ι // y ≠ x } := Finset.subtype (fun (x_1 : ι) ↦ x_1 ≠ x) s
p' : { y : ι // y ≠ x } → P := fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
his : x ∉ s ∨ w x = 0
w' : { y : ι // y ≠ x } → k := fun (x_1 : { y : ι // y ≠ x }) ↦ w (↑x_1 : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
⊢ False

Tactic:
hwx (his.neg_resolve_left hxs)

Premises used: Or.neg_resolve_left