awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
s : Finset P
w : P → k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
rw₁ :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (Subtype.val (p := fun (x : P) ↦ x ∈ s)) s.attach) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
have rw₂ : Eq.{u_3 + 1} (α := P) ((affineCombination k s id : (a : P → k) → P) w : P)
  ((affineCombination k s id : (a : P → k) → P) w : P)
Tactic: rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
s : Finset P
w : P → k
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
have classical : Eq.{u_3 + 1} (α := P)
  ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
  ((affineCombination k s id : (a : P → k) → P) w : P)
Tactic: classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
s : Finset P
w : P → k
classical :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
have classical₁ : Eq.{u_3 + 1} (α := P)
  ((affineCombination k (image (Subtype.val (p := fun (x : P) ↦ x ∈ s)) s.attach) id : (a : P → k) → P) w : P)
  ((affineCombination k s id : (a : P → k) → P) w : P)
Tactic: classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
s : Finset P
w : P → k
classical :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
classical₁ :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (Subtype.val (p := fun (x : P) ↦ x ∈ s)) s.attach) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
have classical₂ : Eq.{u_3 + 1} (α := P) ((affineCombination k s id : (a : P → k) → P) w : P)
  ((affineCombination k s id : (a : P → k) → P) w : P)
Tactic: classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
⊢ (affineCombination k s p : (a : ι → k) → P) w = p i
have h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
Tactic: have h1 : ∑ i ∈ s, w i = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ (affineCombination k s p : (a : ι → k) → P) w = p i
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) (p i) = p i
Tactic: rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i),
    weightedVSubOfPoint_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) (p i) = p i
have h : Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) 0
Tactic: convert! zero_vadd V (p i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) 0
have h : ∀ x ∈ s, w x • (p x -ᵥ p i) = 0
Tactic: refine sum_eq_zero ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i2 : ι
hi2 : i2 ∈ s
⊢ w i2 • (p i2 -ᵥ p i) = 0
have pos : ∀ (h : i2 = i), w i2 • (p i2 -ᵥ p i) = 0
Tactic: by_cases h : i2 = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i2 : ι
hi2 : i2 ∈ s
pos : ∀ (h : i2 = i), w i2 • (p i2 -ᵥ p i) = 0
⊢ w i2 • (p i2 -ᵥ p i) = 0
have neg : ∀ (h : ¬i2 = i), w i2 • (p i2 -ᵥ p i) = 0
Tactic: by_cases h : i2 = i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s₁ p : (a : ι → k) → P) w : P)
    ((affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w) : P)
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s₁.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V)
    (Classical.choice sorry) =
  (affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w)
Tactic: rw [affineCombination_apply, affineCombination_apply,
    weightedVSubOfPoint_indicator_subset _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₁.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    (affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s₁ p : (a : ι → k) → P) w : P)
    ((affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w) : P)
have rw₁ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s₁.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V)
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s₂.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
    (Classical.choice sorry)
Tactic: rw [affineCombination_apply, affineCombination_apply,
    weightedVSubOfPoint_indicator_subset _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₁.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    (affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₁.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₂.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
      (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s₁ p : (a : ι → k) → P) w : P)
    ((affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w) : P)
have rw₂ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s₂.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s₂.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
    (Classical.choice sorry)
Tactic: rw [affineCombination_apply, affineCombination_apply,
    weightedVSubOfPoint_indicator_subset _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) w : P)
    ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) (w ∘ (⇑e : (a : ι₂) → ι)) : P)
have simp_rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (((map e s₂).weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V) (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s₂.weightedVSubOfPoint (p ∘ (⇑e : (a : ι₂) → ι)) (Classical.choice sorry) : (a : ι₂ → k) → V)
        (w ∘ (⇑e : (a : ι₂) → ι)) :
      V)
    (Classical.choice sorry)
Tactic: simp_rw [affineCombination_apply, weightedVSubOfPoint_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p₁ : (a : ι → k) → P) w : P)
      ((affineCombination k s p₂ : (a : ι → k) → P) w : P)
have simp_rw : ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
  HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ (Classical.choice sorry) : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p₂ (Classical.choice sorry) : (a : ι → k) → V) w : V)
Tactic: simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
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) 1
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
have rw : VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p₁ : (a : ι → k) → P) w : P)
    ((affineCombination k s fun (i : ι) ↦ p₂ : (a : ι → k) → P) w : P) =
  (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
Tactic: rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
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) 1
rw :
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p₁ : (a : ι → k) → P) w : P)
      ((affineCombination k s fun (i : ι) ↦ p₂ : (a : ι → k) → P) w : P) =
    (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
have rw₁ : (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂ = (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
Tactic: rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
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) 1
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
have rw : VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s fun (i : ι) ↦ p₁ : (a : ι → k) → P) w : P)
    ((affineCombination k s p₂ : (a : ι → k) → P) w : P) =
  p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
Tactic: rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
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) 1
rw :
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s fun (i : ι) ↦ p₁ : (a : ι → k) → P) w : P)
      ((affineCombination k s p₂ : (a : ι → k) → P) w : P) =
    p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
have rw₁ : p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w = p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
Tactic: rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ s₂) p : (a : ι → k) → P) w : P)
      ((affineCombination k s₂ p : (a : ι → k) → P) (-w) : P) =
    (s.weightedVSub p : (a : ι → k) → V) w
have simp_rw : HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w : V)
    ((s₂.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) (-w) : V) =
  (s.weightedVSub p : (a : ι → k) → V) w
Tactic: simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
    ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
Tactic: rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
have e_a : p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
have e_a : (-w) i = 1
Tactic: refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
e_a : (-w) i = 1
⊢ p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
have e_a₁ : ∀ (i2 : ι), Membership.mem (γ := Finset ι) {i} i2 → i2 ≠ i → (-w) i2 = 0
Tactic: refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have rw₂ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
    ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (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
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
rw₂ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i
have rw₃ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s.erase i) p : (a : ι → k) → P) w : P)
    ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
Tactic: classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp