no goals
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ w x, p1 = ↑(Finset.affineCombination k Finset.univ p) w
classical
  obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
  refine'
    ⟨(s : Set ι).indicator w, _, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
  simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
  rw [Fintype.sum_extend_by_zero s w]
case intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ w_1 x, ↑(Finset.affineCombination k s p) w = ↑(Finset.affineCombination k Finset.univ p) w_1
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ w x, p1 = ↑(Finset.affineCombination k Finset.univ p) w
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h
case intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i : ι, Set.indicator (↑s) w i = 1
case intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ w_1 x, ↑(Finset.affineCombination k s p) w = ↑(Finset.affineCombination k Finset.univ p) w_1
refine'
  ⟨(s : Set ι).indicator w, _, Finset.affineCombination_indicator_subset w p s.subset_univ⟩
case intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ (∑ x : ι, if x ∈ s then w x else 0) = ∑ i in s, w i
case intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i : ι, Set.indicator (↑s) w i = 1
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]
no goals
case intro.intro.intro
k : Type u_3
V : Type u_4
P : Type u_2
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_1
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 1
h : ↑(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ (∑ x : ι, if x ∈ s then w x else 0) = ∑ i in s, w i
rw [Fintype.sum_extend_by_zero s w]