-- 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
p : ι → P
have have₁ have₂ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₃ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (hn : s.Nonempty),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₄ have₅ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₆ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
    ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1),
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₇ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
    ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1)
      (hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1),
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₈ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
    ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1)
      (hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1)
      (hv :
        Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
          ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)),
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have₉ :
  ∀ (hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0) (i1 : ι) (hi1 : i1 ∈ s),
    let w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1;
    ∀ (hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1)
      (hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1)
      (hv :
        Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
          ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)),
      Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        (((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1) +ᵥ p i1)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))