-- 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
p₁ : P
p : ι → P
s : Set ι
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s)) p₁
rw rw₁ rw₂ :
  ∀ (h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι))) p₁),
    ∃ (fs : Finset ι) (w : ι → k),
      (↑fs : Set ι) ⊆ s ∧
        Eq.{u_2 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p₁ = (Finset.affineCombination k fs p : (a : ι → k) → P) w
rw₃ :
  ∀ (fs' : Finset (↑s : Type u_1)) (w' : (↑s : Type u_1) → k) (hw' : Eq.{u_2 + 1} (α := k) (∑ i ∈ fs', w' i) 1)
    (h :
      Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
        (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι)))
        ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' :
          P)),
    ∃ (fs : Finset ι) (w : ι → k),
      (↑fs : Set ι) ⊆ s ∧
        Eq.{u_2 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_4 + 1} (α := P)
            ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P)
                w' :
              P)
            ((Finset.affineCombination k fs p : (a : ι → k) → P) w : P)
rw₄ :
  ∀ (fs' : Finset (↑s : Type u_1)) (w' : (↑s : Type u_1) → k) (hw' : Eq.{u_2 + 1} (α := k) (∑ i ∈ fs', w' i) 1)
    (h :
      Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
        (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι)))
        ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' :
          P)),
    Eq.{u_4 + 1} (α := P)
      ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' : P)
      ((Finset.affineCombination k (Finset.map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs') p :
            (a : ι → k) → P)
          fun (i : ι) ↦ if hi : i ∈ s then w' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else 0 :
        P)
rw₅ :
  ∀ (fs' : Finset (↑s : Type u_1)) (w' : (↑s : Type u_1) → k) (hw' : Eq.{u_2 + 1} (α := k) (∑ i ∈ fs', w' i) 1)
    (h :
      Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P)
        (affineSpan k (Set.range fun (x : (↑s : Type u_1)) ↦ p (↑x : ι)))
        ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' :
          P)),
    Eq.{u_4 + 1} (α := P)
      ((Finset.affineCombination k fs' fun (x : (↑s : Type u_1)) ↦ p (↑x : ι) : (a : (↑s : Type u_1) → k) → P) w' : P)
      ((Finset.affineCombination k fs' (p ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : { x : ι // x ∈ s } → k) → P)
          ((fun (i : ι) ↦ if hi : i ∈ s then w' (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else 0) ∘
            Subtype.val (p := fun (x : ι) ↦ x ∈ s)) :
        P)
⊢ ∃ (fs : Finset ι) (w : ι → k),
    (↑fs : Set ι) ⊆ s ∧
      Eq.{u_2 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p₁ = (Finset.affineCombination k fs p : (a : ι → k) → P) w

Tactic:
classical
  rw [Set.image_eq_range] at h
  obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h
  refine ⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0,
    (by simp), (by simp [hw']), ?_⟩
  simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]
  exact fs'.affineCombination_congr (by simp) (by simp)

Premises used: Function.Embedding.coe_subtype, Finset.affineCombination_map, Set.image_eq_range, eq_affineCombination_of_mem_affineSpan, rfl