-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
have have₁ have₂ :
  ∀ (hn : (↑(affineSpan k (Set.range p)) : Set P).Nonempty),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₃ :
  ∀ (hn : Nonempty ι),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₄ :
  ∀ (i0 : ι),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₅ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₆ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0))
    (hd : Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p))) (p1 -ᵥ p i0)),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₇ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0))
    (hd :
      ∃ (s : Finset ι) (w : ι → k),
        Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₈ have₉ have₁₀ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    ∃ (s : Finset ι) (w : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₁₁ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    let s' := insert i0 s;
    let w' := (↑s : Set ι).indicator w;
    ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0),
      ∃ (s : Finset ι) (w : ι → k),
        Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₁₂ have₁₃ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    let s' := insert i0 s;
    let w' := (↑s : Set ι).indicator w;
    ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0) (hs' : (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0),
      ∃ (s : Finset ι) (w : ι → k),
        Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₁₄ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    let s' := insert i0 s;
    let w' := (↑s : Set ι).indicator w;
    ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0) (hs' : (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0),
      let w0 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 1;
      ∀ (hw0 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1),
        ∃ (s : Finset ι) (w : ι → k),
          Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have₁₅ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    let s' := insert i0 s;
    let w' := (↑s : Set ι).indicator w;
    ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0) (hs' : (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0),
      let w0 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 1;
      ∀ (hw0 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1)
        (hw0s : (Finset.affineCombination k s' p : (a : ι → k) → P) w0 = p i0),
        ∃ (s : Finset ι) (w : ι → k),
          Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
refine_1 :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    let s' := insert i0 s;
    let w' := (↑s : Set ι).indicator w;
    ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0) (hs' : (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0),
      let w0 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 1;
      ∀ (hw0 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1)
        (hw0s : (Finset.affineCombination k s' p : (a : ι → k) → P) w0 = p i0),
        Eq.{u_2 + 1} (α := k) (∑ i ∈ s', (w0 + w') i) 1
refine_2 refine_2₁ :
  ∀ (i0 : ι) (h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)) (s : Finset ι)
    (w : ι → k) (h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hs : p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w),
    let s' := insert i0 s;
    let w' := (↑s : Set ι).indicator w;
    ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0) (hs' : (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0),
      let w0 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 1;
      ∀ (hw0 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1)
        (hw0s : (Finset.affineCombination k s' p : (a : ι → k) → P) w0 = p i0),
        p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')
⊢ ∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w

Tactic:
classical
    have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
    rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn
    obtain ⟨i0⟩ := hn
    have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
    have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction :=
      AffineSubspace.vsub_mem_direction h h0
    rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd
    rcases hd with ⟨s, w, h, hs⟩
    let s' := insert i0 s
    let w' := Set.indicator (↑s) w
    have h' : ∑ i ∈ s', w' i = 0 := by
      rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]
    have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
      rw [hs]
      exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
    let w0 : ι → k := Function.update (Function.const ι 0) i0 1
    have hw0 : ∑ i ∈ s', w0 i = 1 := by
      rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
      simp only [Function.const_apply, Finset.sum_const_zero,
        add_zero]
    have hw0s : s'.affineCombination k p w0 = p i0 :=
      s'.affineCombination_of_eq_one_of_eq_zero w0 p (Finset.mem_insert_self _ _)
        (Function.update_self ..) fun _ _ hne => Function.update_of_ne hne _ _
    refine ⟨s', w0 + w', ?_, ?_⟩
    · simp [Pi.add_apply, Finset.sum_add_distrib, hw0, h']
    · rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]

Premises used: Set.range_nonempty_iff_nonempty, direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub, Finset.sum_add_distrib, add_comm, Pi.add_apply, Finset.weightedVSub_vadd_affineCombination, affineSpan_nonempty, vsub_vadd