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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)) ↔ ∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)
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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs x_1 w x, v = ↑(weightedVSubOfPoint fs p b) w) ↔ ∃ fs w x, v = ↑(weightedVSubOfPoint fs (fun i => p ↑i) b) w
simp_rw [weightedVSubOfPoint_apply]
case mp
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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)) → ∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)

case mpr
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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)) → ∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)
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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)) ↔ ∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)
constructor
case mp.intro.intro.intro.intro
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.373025
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ι
hfs : ↑fs ⊆ s
w : ι → k
⊢ ∃ fs_1 w_1 h, ∑ i in fs, w i • (p i -ᵥ b) = ∑ i in fs_1, w_1 i • (p ↑i -ᵥ b)
case mp
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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)) → ∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)
rintro ⟨fs, hfs, w, rfl, rfl⟩
no goals
case mp.intro.intro.intro.intro
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.373025
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ι
hfs : ↑fs ⊆ s
w : ι → k
⊢ ∃ fs_1 w_1 h, ∑ i in fs, w i • (p i -ᵥ b) = ∑ i in fs_1, w_1 i • (p ↑i -ᵥ b)
exact ⟨fs.subtype s, fun i => w i, sum_subtype_of_mem _ hfs, (sum_subtype_of_mem _ hfs).symm⟩
case mpr.intro.intro.intro
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.373025
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∃ fs_1 h w_1 h, ∑ i in fs, w i • (p ↑i -ᵥ b) = ∑ i in fs_1, w_1 i • (p i -ᵥ b)
case mpr
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.373025
s₂ : Finset ι₂
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs w h, v = ∑ i in fs, w i • (p ↑i -ᵥ b)) → ∃ fs h w h, v = ∑ i in fs, w i • (p i -ᵥ b)
rintro ⟨fs, w, rfl, rfl⟩
no goals
case mpr.intro.intro.intro
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.373025
s₂ : Finset ι₂
s : Set ι
p : ι → P
b : P
fs : Finset ↑s
w : ↑s → k
⊢ ∃ fs_1 h w_1 h, ∑ i in fs, w i • (p ↑i -ᵥ b) = ∑ i in fs_1, w_1 i • (p i -ᵥ b)
refine'
    ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
      if h : i ∈ s then w ⟨i, h⟩ else 0, _, _⟩ <;>
  simp