awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
v : V
p : ι → P
mp :
  Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w
mpr mpr₁ :
  (∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w) →
    Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (Set.range p)) v ↔
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
classical
    constructor
    · rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
      swap
      · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
          Finsupp.mem_span_image_iff_linearCombination]
        rintro ⟨l, _, hv⟩
        use insert i0 l.support
        set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef
        use w
        have hw : ∑ i ∈ insert i0 l.support, w i = 0 := by
          rw [hwdef]
          simp_rw [Pi.sub_apply, Finset.sum_sub_distrib,
            Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
            Finset.sum_insert_of_eq_zero_if_notMem Finsupp.notMem_support_iff.1]
          simp only [Function.const_apply, Finset.sum_const_zero, add_zero, sub_self]
        use hw
        have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
        change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz
        rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0),
          Finset.weightedVSubOfPoint_apply, ← hv, Finsupp.linearCombination_apply,
          @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
        change (∑ i ∈ l.support, l i • _) = _
        congr with i
        by_cases h : i = i0
        · simp [h]
        · simp [hwdef, h]
      · rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
        rintro rfl
        use ∅
        simp
    · rintro ⟨s, w, hw, rfl⟩
      exact weightedVSub_mem_vectorSpan hw p

Premises used: Finset.weightedVSubOfPoint_apply, Set.image_univ, Submodule.mem_bot, vectorSpan_empty, isEmpty_or_nonempty, Finsupp.linearCombination_apply, Finsupp.mem_span_image_iff_linearCombination, Set.range_eq_empty, rfl
-- 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
⊢ (↑(affineSpan k (Set.range p)) : Set P).Nonempty

Tactic:
have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
-- 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
hn : (↑(affineSpan k (Set.range p)) : Set P).Nonempty
⊢ Nonempty ι

Tactic:
rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn

Premises used: Set.range_nonempty_iff_nonempty, affineSpan_nonempty
-- 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
hn : Nonempty ι
obtain :
  ∀ (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
⊢ ∃ (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:
obtain ⟨i0⟩ := hn
-- 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
i0 : ι
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)

Tactic:
have h0 : p i0 ∈ affineSpan k (Set.range p) := mem_affineSpan k (Set.mem_range_self i0)
-- 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
i0 : ι
h0 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (p i0)
⊢ Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p))) (p1 -ᵥ p i0)

Tactic:
have hd : p1 -ᵥ p i0 ∈ (affineSpan k (Set.range p)).direction :=
      AffineSubspace.vsub_mem_direction h h0
-- 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
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) 0 ∧ p1 -ᵥ p i0 = (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd

Premises used: direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub
-- 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
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
rcases :
  ∀ (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
⊢ ∃ (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:
rcases hd with ⟨s, w, h, hs⟩
-- 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_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
rw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) (∑ i ∈ s, w i)
rw₁ rw₂ : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) (∑ i ∈ s, w i)
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0

Tactic:
rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]

Premises used: Finset.sum_indicator_subset, Finset.subset_insert
-- 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_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
⊢ 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)]
-- 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_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
rw : Eq.{u_3 + 1} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)
⊢ (s'.weightedVSub p : (a : ι → k) → V) w' = p1 -ᵥ p i0

Tactic:
rw [hs]
-- 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_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
⊢ Eq.{u_3 + 1} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
(Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm

Premises used: Finset.subset_insert, Eq.symm, Finset.weightedVSub_indicator_subset
-- 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_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
⊢ Eq.{u_3 + 1} (α := V) ((s'.weightedVSub p : (a : ι → k) → V) w' : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm

Premises used: Finset.subset_insert, Eq.symm, Finset.weightedVSub_indicator_subset
-- 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_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

Tactic:
have hs' : s'.weightedVSub p w' = p1 -ᵥ p i0 := by
      rw [hs]
      exact (Finset.weightedVSub_indicator_subset _ _ (Finset.subset_insert i0 s)).symm
-- 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_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
rw : HAdd.hAdd (α := k) 1 (∑ x ∈ insert i0 s \ {i0}, Function.const ι 0 x) = 1
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w0 i) 1

Tactic:
rw [Finset.sum_update_of_mem (Finset.mem_insert_self _ _)]

Premises used: Finset.mem_insert_self, Finset.sum_update_of_mem
-- 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_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
⊢ HAdd.hAdd (α := k) 1 (∑ x ∈ insert i0 s \ {i0}, Function.const ι 0 x) = 1

Tactic:
simp only [Function.const_apply, Finset.sum_const_zero,
        add_zero]

Premises used: Function.const_apply, Finset.sum_const_zero, add_zero
-- 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_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

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]
-- 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_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
⊢ (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 _ _
-- 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_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

Tactic:
⟨s', w0 + w', ?_, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro
-- 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_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
refine_2 : 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:
refine ⟨s', w0 + w', ?_, ?_⟩
-- 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_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
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s', (w0 + w') i) 1

Tactic:
simp [Pi.add_apply, Finset.sum_add_distrib, hw0, h']

Premises used: Finset.sum_add_distrib, Pi.add_apply
-- 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_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
refine_2₄ refine_2₅ : p1 = p1
⊢ p1 = (Finset.affineCombination k s' p : (a : ι → k) → P) (w0 + w')

Tactic:
rw [add_comm, ← Finset.weightedVSub_vadd_affineCombination, hw0s, hs', vsub_vadd]

Premises used: add_comm, Finset.weightedVSub_vadd_affineCombination, vsub_vadd
-- 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 : Fintype ι
p1 : P
p : ι → P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
obtain :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1)
    (h :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
        ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)),
    ∃ (w_1 : ι → k),
      Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
        Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
          ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w i) 1 ∧ p1 = (Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w

Tactic:
obtain ⟨s, w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan h

Premises used: eq_affineCombination_of_mem_affineSpan, rfl
-- 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 : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ ∃ (w_1 : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
      Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
        ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)

Tactic:
⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩

Premises used: Set.indicator, Finset.affineCombination_indicator_subset, SetLike.coe, And.intro, Exists.intro, Finset.subset_univ
-- 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 : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (_root_.Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
Set : Eq.{u_2 + 1} (α := k) (∑ i : ι, (↑s : _root_.Set ι).indicator w i) 1
⊢ ∃ (w_1 : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i : ι, w_1 i) 1 ∧
      Eq.{u_4 + 1} (α := P) ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
        ((Finset.affineCombination k Finset.univ p : (a : ι → k) → P) w_1 : P)

Tactic:
refine
      ⟨(s : Set ι).indicator w, ?_, Finset.affineCombination_indicator_subset w p s.subset_univ⟩