-- 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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
rw rw₁ rw₂ :
  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 s p : (a : ι → k) → P) w : P)
rw₃ :
  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 s p : (a : ι → k) → P) w : P)
rw₄ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s with i ∈ s', w i) 1),
    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 s p : (a : ι → k) → P) w : P)
rw₅ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
    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 s p : (a : ι → k) → P) w : P)
h₁ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
    Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
      ((Finset.affineCombination k (Finset.subtype (Membership.mem s') s) fun (x : Subtype (Membership.mem s')) ↦
              p (↑x : ι) :
            (a : Subtype (Membership.mem s') → k) → P)
          fun (i : Subtype (Membership.mem s')) ↦ w (↑i : ι) :
        P)
h₂ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1),
    Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
      ((Finset.affineCombination k s p : (a : ι → k) → P) ((↑({x ∈ s | x ∈ s'}) : Set ι).indicator w) : P)
h₃ :
  ∀ (h' : Eq.{u_2 + 1} (α := k) (∑ x ∈ Finset.subtype (Membership.mem s') s, w (↑x : ι)) 1) (i : ι) (hi : i ∈ s),
    w i = (↑({x ∈ s | x ∈ s'}) : Set ι).indicator w i
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s'))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
classical
  rw [Set.image_eq_range]
  let w' : s' → k := fun i ↦ w i
  have h' : ∑ i ∈ s with i ∈ s', w i = 1 := by
    rw [← h, ← Finset.sum_sdiff (s₁ := {x ∈ s | x ∈ s'}) (s₂ := s) (by simp), right_eq_add]
    refine Finset.sum_eq_zero ?_
    intro i hi
    simp only [Finset.mem_sdiff, Finset.mem_filter, not_and] at hi
    exact hs' i hi.1 (hi.2 hi.1)
  rw [← Finset.sum_subtype_eq_sum_filter] at h'
  convert! affineCombination_mem_affineSpan h' (fun x ↦ p x)
  rw [Finset.affineCombination_subtype_eq_filter, Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)]
  refine Finset.affineCombination_congr _ (fun i hi ↦ ?_) (fun _ _ ↦ rfl)
  simp_all [Set.indicator_apply]

Premises used: Set.indicator_apply, Finset.affineCombination_congr, Finset.filter_subset, Finset.affineCombination_indicator_subset, Set.image_eq_range, Finset.sum_subtype_eq_sum_filter, rfl, Finset.affineCombination_subtype_eq_filter