-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem eq_affineCombination_of_mem_affineSpan_of_fintype [Fintype ι] {p1 : P} {p : ι → P}
    (h : p1 ∈ affineSpan k (Set.range p)) :
    ∃ w : ι → k, ∑ i, w i = 1 ∧ p1 = Finset.univ.affineCombination k p w

Proof state:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ w, ∑ i : ι, w i = 1 ∧ p1 = (Finset.affineCombination k Finset.univ p) w

Tactic:
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h

Result:
case intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ w_1, ∑ i : ι, w_1 i = 1 ∧ (Finset.affineCombination k s p) w = (Finset.affineCombination k Finset.univ p) w_1

Proof state:
case intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∃ w_1, ∑ i : ι, w_1 i = 1 ∧ (Finset.affineCombination k s p) w = (Finset.affineCombination k Finset.univ p) w_1

Tactic:
refine
  ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩

Result:
case intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i : ι, (↑s).indicator w i = 1

Proof state:
case intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
h : (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
⊢ ∑ i : ι, (↑s).indicator w i = 1

Tactic:
simp only [Finset.mem_coe, Set.indicator_apply, ← hw]

Result:
case intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ 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 ∈ s, w i

Proof state:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p1 : P
p : ι → P
h : p1 ∈ affineSpan k (Set.range p)
⊢ ∃ w, ∑ i : ι, w i = 1 ∧ p1 = (Finset.affineCombination k Finset.univ p) w

Tactic:
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]

Result:
no goals

Proof state:
case intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ 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 ∈ s, w i

Tactic:
rw [Fintype.sum_extend_by_zero s w]

Result:
no goals