k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ↑(affineCombination k (filter (fun x => x ≠ i) s) p) w -ᵥ p i =
    ↑(affineCombination k (filter (fun a => a ≠ i) s) p) w -ᵥ ↑(affineCombination k {i} p) (-w)
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ↑(affineCombination k (filter (fun x => x ≠ i) s) p) w = p i
rw [← @vsub_eq_zero_iff_eq V, ← hw,
  ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
  ← filter_ne']
case e_a
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = ↑(affineCombination k {i} p) (-w)
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ↑(affineCombination k (filter (fun x => x ≠ i) s) p) w -ᵥ p i =
    ↑(affineCombination k (filter (fun a => a ≠ i) s) p) w -ᵥ ↑(affineCombination k {i} p) (-w)
congr
case e_a.refine'_1
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (-w) i = 1

case e_a.refine'_2
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ (i2 : ι), i2 ∈ {i} → i2 ≠ i → (-w) i2 = 0
case e_a
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = ↑(affineCombination k {i} p) (-w)
refine' (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) _ _).symm
no goals
case e_a.refine'_1
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (-w) i = 1
simp [hwi]
no goals
case e_a.refine'_2
k : Type u_3
V : Type u_1
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.357197
s₂ : Finset ι₂
w : ι → k
p : ι → P
hw : ↑(weightedVSub s p) w = 0
i : ι
inst✝ : DecidablePred fun x => x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ (i2 : ι), i2 ∈ {i} → i2 ≠ i → (-w) i2 = 0
simp