awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑s : Set ι).indicator 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 h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0
Tactic: have h' : ∑ i ∈ s', w' i = 0 := by
      rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑s : Set ι).indicator w
h' : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0
⊢ (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0
have rw : Eq.{u_3 + 1} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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 hs' : (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0
Tactic: have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
      rw [hs]
      exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
w0 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 1
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1
have rw : HAdd.hAdd (α := k) 1 (∑ x ∈ insert i0 s \ {i0}, Function.const ι 0 x) = 1
Tactic: rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
w0 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 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 hw0 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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 hw0s : (Finset.affineCombination k s' p : (a : ι → k) → P) w0 = p i0
Tactic: 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 _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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
have refine_1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', (w0 + w') i) 1
Tactic: refine ⟨s', w0 + w', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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
refine_1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', (w0 + w') 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 refine_2 : p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')
Tactic: refine ⟨s', w0 + w', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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')
have refine_2 : p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w' + w0)
Tactic: rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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
refine_2 : p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w' + w0)
⊢ p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')
have refine_2₁ : p1 =
  HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P) ((s'.weightedVSub p : (a : ι → k) → V) w' : V)
    ((Finset.affineCombination k s' p : (a : ι → k) → P) w0 : P)
Tactic: rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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
refine_2 : p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w' + w0)
refine_2₁ :
  p1 =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P) ((s'.weightedVSub p : (a : ι → k) → V) w' : V)
      ((Finset.affineCombination k s' p : (a : ι → k) → P) w0 : P)
⊢ p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')
have refine_2₂ : p1 = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) (p i0)
Tactic: rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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
refine_2 : p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w' + w0)
refine_2₁ :
  p1 =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P) ((s'.weightedVSub p : (a : ι → k) → V) w' : V)
      ((Finset.affineCombination k s' p : (a : ι → k) → P) w0 : P)
refine_2₂ : p1 = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) (p i0)
⊢ p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')
have refine_2₃ : p1 = (p1 -ᵥ p i0) +ᵥ p i0
Tactic: rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι := insert i0 s
w' : (x : ι) → k := (↑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
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
refine_2 : p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w' + w0)
refine_2₁ :
  p1 =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P) ((s'.weightedVSub p : (a : ι → k) → V) w' : V)
      ((Finset.affineCombination k s' p : (a : ι → k) → P) w0 : P)
refine_2₂ : p1 = HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) (p i0)
refine_2₃ : p1 = (p1 -ᵥ p i0) +ᵥ p i0
⊢ p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')
have refine_2₄ : p1 = p1
Tactic: rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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 : ∀ (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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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₃ : ∀ (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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ ∃ (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 : ι),
  ∃ (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]