awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
w : ι → k
p : ι → P
i : ι
rw : Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))
⊢ Eq.{u_2 + 1} (α := V) (((s.erase i).weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
w : ι → k
p : ι → P
i : ι
h : w i • (p i -ᵥ p i) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))

Tactic:
apply sum_erase

Premises used: Finset.sum_erase
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
w : ι → k
p : ι → P
i : ι
h : HSMul.hSMul (β := V) (w i) 0 = 0
h₁ h₂ : Eq.{u_2 + 1} (α := V) 0 0
⊢ w i • (p i -ᵥ p i) = 0

Tactic:
rw [vsub_self, smul_zero]

Premises used: smul_zero, vsub_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
w : ι → k
p : ι → P
i : ι
rw : Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))
⊢ Eq.{u_2 + 1} (α := V) (((insert i s).weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (p i) : (a : ι → k) → V) w : V)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
w : ι → k
p : ι → P
i : ι
h : w i • (p i -ᵥ p i) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ insert i s, w i_1 • (p i_1 -ᵥ p i)) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i))

Tactic:
apply sum_insert_zero

Premises used: Finset.sum_insert_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
rw : Eq.{u_2 + 1} (α := V) (∑ i ∈ s₁, w i • (p i -ᵥ b)) (∑ i ∈ s₂, (↑s₁ : Set ι).indicator w i • (p i -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V) ((s₁.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s₁, w i • (p i -ᵥ b)) (∑ i ∈ s₂, (↑s₁ : Set ι).indicator w i • (p i -ᵥ b))

Tactic:
Eq.symm <|
    sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

Premises used: Finset.sum_indicator_subset_of_eq_zero, VSub.vsub, zero_smul, HSMul.hSMul, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s₁, w i • (p i -ᵥ b)) (∑ i ∈ s₂, (↑s₁ : Set ι).indicator w i • (p i -ᵥ b))

Tactic:
exact Eq.symm <|
    sum_indicator_subset_of_eq_zero w (fun i wi => wi • (p i -ᵥ b : V)) h fun i => zero_smul k _

Premises used: Finset.sum_indicator_subset_of_eq_zero, VSub.vsub, zero_smul, HSMul.hSMul, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
simp_rw :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ map e s₂, w i • (p i -ᵥ b))
    (∑ i ∈ s₂, (w ∘ (⇑e : (a : ι₂) → ι)) i • ((p ∘ (⇑e : (a : ι₂) → ι)) i -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V) (((map e s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s₂.weightedVSubOfPoint (p ∘ (⇑e : (a : ι₂) → ι)) b : (a : ι₂ → k) → V) (w ∘ (⇑e : (a : ι₂) → ι)) : V)

Tactic:
simp_rw [weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ map e s₂, w i • (p i -ᵥ b))
    (∑ i ∈ s₂, (w ∘ (⇑e : (a : ι₂) → ι)) i • ((p ∘ (⇑e : (a : ι₂) → ι)) i -ᵥ b))

Tactic:
Finset.sum_map _ _ _

Premises used: Finset.sum_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ map e s₂, w i • (p i -ᵥ b))
    (∑ i ∈ s₂, (w ∘ (⇑e : (a : ι₂) → ι)) i • ((p ∘ (⇑e : (a : ι₂) → ι)) i -ᵥ b))

Tactic:
exact Finset.sum_map _ _ _

Premises used: Finset.sum_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
b : P
simp_rw : ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = HSub.hSub (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ b)) (∑ i ∈ s, w i • (p₂ i -ᵥ b))
simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) (∑ x ∈ s, (w x • (p₁ x -ᵥ b) - w x • (p₂ x -ᵥ b)))
simp_rw₂ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) (∑ x ∈ s, w x • (p₁ x -ᵥ b - (p₂ x -ᵥ b)))
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)

Tactic:
simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]

Premises used: Finset.weightedVSubOfPoint_apply, smul_sub, Finset.sum_sub_distrib, vsub_sub_vsub_cancel_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ b : P
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint (fun (i : ι) ↦ p₂) b : (a : ι → k) → V) w : V) =
    HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))
b₁ : P
rw₁ :
  HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b)) =
    HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))
b₂ : P
rw₂ :
  HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b)) =
    HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))
b₃ : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) =
    HSub.hSub (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w : V)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₂ -ᵥ b))

Tactic:
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

Premises used: Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub, Finset.weightedVSubOfPoint_apply_const
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ b : P
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint (fun (i : ι) ↦ p₁) b : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
b₁ : P
rw₁ :
  HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
b₂ : P
rw₂ :
  HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)
b₃ : P
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) =
    HSub.hSub (β := V) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p₁ -ᵥ b))
      ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w : V)

Tactic:
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

Premises used: Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub, Finset.weightedVSubOfPoint_apply_const
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
simp_rw : HAdd.hAdd (α := V) (∑ i ∈ s \ s₂, w i • (p i -ᵥ b)) (∑ i ∈ s₂, w i • (p i -ᵥ b)) = ∑ i ∈ s, w i • (p i -ᵥ b)
⊢ HAdd.hAdd (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w

Tactic:
simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.sum_sdiff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
rw :
  HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      (-(s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
rw₁ :
  HAdd.hAdd (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
⊢ HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p b : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSubOfPoint p b : (a : ι → k) → V) w

Tactic:
rw [map_neg, sub_neg_eq_add, s.weightedVSubOfPoint_sdiff h]

Premises used: Finset.weightedVSubOfPoint_sdiff, map_neg, sub_neg_eq_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
rw :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b) : V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
rw₁ :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b))
    (∑ i ∈ s with pred i, w i • (p i -ᵥ b))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ Finset.subtype pred s, w (↑i : ι) • (p (↑i : ι) -ᵥ b))
    (∑ x ∈ Finset.subtype pred s, w (↑x : ι) • (p (↑x : ι) -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V)
    (((Finset.subtype pred s).weightedVSubOfPoint (fun (i : Subtype pred) ↦ p (↑i : ι)) b : (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_subtype_eq_sum_filter]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.sum_subtype_eq_sum_filter
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
rw : ∀ x ∈ s, w x • (p x -ᵥ b) ≠ 0 → pred x
⊢ Eq.{u_2 + 1} (α := V) (({x ∈ s | pred x}.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, sum_filter_of_ne]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.sum_filter_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ pred i

Tactic:
h i hi ?_
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
refine : w i ≠ 0
⊢ pred i

Tactic:
refine h i hi ?_
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
hw : w i = 0
⊢ False

Tactic:
simp [hw] at hne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
simp_rw : ∑ i ∈ s, (c • w) i • (p i -ᵥ b) = HSMul.hSMul (β := V) c (∑ i ∈ s, w i • (p i -ᵥ b))
simp_rw₁ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, (c • w) i • (p i -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
simp_rw₂ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (c • w x) • (p x -ᵥ b)) (∑ x ∈ s, c • w x • (p x -ᵥ b))
simp_rw₃ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (c • w x) • (p x -ᵥ b)) (∑ x ∈ s, (c * w x) • (p x -ᵥ b))
⊢ (s.weightedVSubOfPoint p b : (a : ι → k) → V) (c • w) =
    HSMul.hSMul (β := V) c ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)

Tactic:
simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]

Premises used: Finset.weightedVSubOfPoint_apply, smul_smul, Finset.smul_sum, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (∑ i ∈ s, w i • (p i -ᵥ Classical.choice ⋯) : V)

Tactic:
simp [weightedVSub]

Premises used: Finset.weightedVSub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b : P
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V)

Tactic:
s.weightedVSubOfPoint_eq_of_sum_eq_zero w p h _ _

Premises used: Finset.weightedVSubOfPoint_eq_of_sum_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  Eq.{u_2 + 1} (α := V)
    ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V) w :
      V)
    (0 : V)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯) = 0
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (p -ᵥ Classical.choice ⋯) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := V) 0 0
⊢ Eq.{u_2 + 1} (α := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (x : ι) ↦ p : (a : ι → k) → V) w : V) (0 : V)

Tactic:
rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]

Premises used: zero_smul, Finset.weightedVSubOfPoint_apply_const, Finset.weightedVSub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
⊢ Eq.{u_2 + 1} (α := V) ((weightedVSub ∅ p : (a : ι → k) → V) w : V) (0 : V)

Tactic:
simp [weightedVSub_apply]

Premises used: Finset.weightedVSub_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
v : V
rw :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint (v +ᵥ p) (Classical.choice ⋯) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₁ :
  Eq.{u_2 + 1} (α := V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₂ :
  Eq.{u_2 + 1} (α := V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
rw₃ : P
rw₄ :
  Eq.{u_2 + 1} (α := V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (HVAdd.hVAdd (β := P) (-v) (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
rw₅ : P
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub (v +ᵥ p) : (a : ι → k) → V) w : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
rw [weightedVSub, weightedVSubOfPoint_vadd,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Premises used: Finset.weightedVSubOfPoint_vadd, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, Finset.weightedVSub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
G : Type u_6
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
s : Finset ι
w : ι → k
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → V
a : G
rw :
  (s.weightedVSubOfPoint (a • p) (Classical.choice ⋯) : (a : ι → k) → V) w =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₁ :
  HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V) =
    HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)
rw₂ :
  HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V) =
    HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
rw₃ : V
rw₄ :
  HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V) =
    HSMul.hSMul (β := V) a
      ((s.weightedVSubOfPoint p (HSMul.hSMul (β := V) a⁻¹ (Classical.choice ⋯)) : (a : ι → k) → V) w : V)
rw₅ : V
⊢ (s.weightedVSub (a • p) : (a : ι → k) → V) w = HSMul.hSMul (β := V) a ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
rw [weightedVSub, weightedVSubOfPoint_smul,
    weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Premises used: Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, Finset.weightedVSubOfPoint_smul, Finset.weightedVSub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w₁ : V) ((s.weightedVSub p₂ : (a : ι → k) → V) w₂ : V)

Tactic:
s.weightedVSubOfPoint_congr hw hp _

Premises used: Finset.weightedVSubOfPoint_congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ Eq.{u_2 + 1} (α := V) ((s₁.weightedVSub p : (a : ι → k) → V) w : V)
    ((s₂.weightedVSub p : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)

Tactic:
weightedVSubOfPoint_indicator_subset _ _ _ h

Premises used: Finset.weightedVSubOfPoint_indicator_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
⊢ Eq.{u_2 + 1} (α := V) (((map e s₂).weightedVSub p : (a : ι → k) → V) w : V)
    ((s₂.weightedVSub (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → V) (w ∘ (⇑e : (a : ι₂) → ι)) : V)

Tactic:
s₂.weightedVSubOfPoint_map _ _ _ _

Premises used: Finset.weightedVSubOfPoint_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSub p₂ : (a : ι → k) → V) w : V)

Tactic:
s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

Premises used: Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
      ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₂ : (a : ι → k) → V) w : V) =
    (s.weightedVSub p₁ : (a : ι → k) → V) w
rw₁ :
  HSub.hSub (α := V) (β := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V) (0 : V) =
    (s.weightedVSub p₁ : (a : ι → k) → V) w
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ i -ᵥ p₂) : V) ((s.weightedVSub p₁ : (a : ι → k) → V) w : V)

Tactic:
rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]

Premises used: Finset.weightedVSub_apply_const, sub_zero, Finset.sum_smul_vsub_eq_weightedVSub_sub