k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ∀ (x : ι), x ∈ s → w x • (p x -ᵥ b) ≠ 0 → pred x
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ↑(weightedVSubOfPoint (filter pred s) p b) w = ↑(weightedVSubOfPoint s p b) w
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, sum_filter_of_ne]
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ pred i
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
⊢ ∀ (x : ι), x ∈ s → w x • (p x -ᵥ b) ≠ 0 → pred x
intro i hi hne
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ w i ≠ 0
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ pred i
refine' h i hi _
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
hw : w i = 0
⊢ False
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
⊢ w i ≠ 0
intro hw
no goals
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.128800
s₂ : Finset ι₂
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ (i : ι), i ∈ s → w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
hw : w i = 0
⊢ False
simp [hw] at hne