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
inst_4 : Nonempty ι
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hn : Nontrivial k
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
exact affineCombination_mem_affineSpan h p

Premises used: affineCombination_mem_affineSpan
-- 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 :
  (∃ (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:
constructor
-- 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 :
  ∀ (hι : IsEmpty ι),
    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
mp₁ :
  ∀ (i0 : ι),
    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
⊢ 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:
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)

Premises used: isEmpty_or_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
v : V
p : ι → P
i0 : ι
mp :
  (∃ (l : ι →₀ k),
      Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l ∧
        (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v) →
    ∃ (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 →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
          Finsupp.mem_span_image_iff_linearCombination]

Premises used: Set.image_univ, vectorSpan_range_eq_span_range_vsub_right, Finsupp.mem_span_image_iff_linearCombination
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
h :
  ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
      v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
⊢ ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
use insert i0 l.support

Premises used: Finsupp.support, Insert.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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
⊢ let w :=
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i));
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))

Tactic:
set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef

Premises used: Function.update, Finsupp.support, Function.const, OfNat.ofNat, DFunLike.coe, Finset.sum
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
h :
  Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
    v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
      v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w

Tactic:
use 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
rw :
  Eq.{u_2 + 1} (α := k)
    (∑ i ∈ insert i0 l.support,
      HSub.hSub (α := (a : ι) → k) (β := (a : ι) → k) (⇑l : (a : ι) → k)
        (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i)) i)
    0
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0

Tactic:
rw [hwdef]
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
simp_rw :
  ∑ x ∈ l.support, (l : (a : ι) → k) x -
      HAdd.hAdd (α := k) (∑ i ∈ l.support, (l : (a : ι) → k) i)
        (∑ x ∈ insert i0 l.support \ {i0}, Function.const ι 0 x) =
    0
⊢ Eq.{u_2 + 1} (α := k)
    (∑ i ∈ insert i0 l.support,
      HSub.hSub (α := (a : ι) → k) (β := (a : ι) → k) (⇑l : (a : ι) → k)
        (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i)) i)
    0

Tactic:
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]

Premises used: Finset.mem_insert_self, Finsupp.notMem_support_iff, Finset.sum_insert_of_eq_zero_if_notMem, Finset.sum_sub_distrib, Finset.sum_update_of_mem, Iff.mp, Pi.sub_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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
⊢ ∑ x ∈ l.support, (l : (a : ι) → k) x -
      HAdd.hAdd (α := k) (∑ i ∈ l.support, (l : (a : ι) → k) i)
        (∑ x ∈ insert i0 l.support \ {i0}, Function.const ι 0 x) =
    0

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

Premises used: Function.const_apply, sub_self, 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0

Tactic:
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]
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
right : v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
    v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w

Tactic:
use hw
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
⊢ w i0 • (p i0 -ᵥ p i0) = 0

Tactic:
have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : w i0 • (p i0 -ᵥ p i0) = 0
⊢ Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0

Tactic:
change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz

Premises used: VSub.vsub, HSMul.hSMul
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0
right : Eq.{u_3 + 1} (α := V) (l.sum fun (i : ι) (a : k) ↦ a • (p i -ᵥ p i0)) (∑ x ∈ l.support, w x • (p x -ᵥ p i0))
⊢ v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w

Tactic:
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]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, Finsupp.linearCombination_apply, Finset.sum_insert_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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0
right :
  Eq.{u_3 + 1} (α := V) (∑ i ∈ l.support, HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0))
    (∑ x ∈ l.support, w x • (p x -ᵥ p i0))
⊢ Eq.{u_3 + 1} (α := V) (l.sum fun (i : ι) (a : k) ↦ a • (p i -ᵥ p i0)) (∑ x ∈ l.support, w x • (p x -ᵥ p i0))

Tactic:
change (∑ i ∈ l.support, l i • _) = _

Premises used: Finsupp.support, HSMul.hSMul, DFunLike.coe, Finset.sum
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0
right : ∀ (i : ι), HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
⊢ Eq.{u_3 + 1} (α := V) (∑ i ∈ l.support, HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0))
    (∑ x ∈ l.support, w x • (p x -ᵥ p i0))

Tactic:
congr with i
-- 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
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0
i : ι
pos : ∀ (h : i = i0), HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
neg :
  ∀ (h : ¬i = i0), HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
by_cases h : i = 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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0
i : ι
h : i = i0
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
simp [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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left : Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l
hv : (Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l = v
w : (a : ι) → k :=
  HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
    (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hwdef :
  w =
    HSub.hSub (α := (a : ι) → k) (⇑l : (a : ι) → k)
      (Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i0 (∑ i ∈ l.support, (l : (a : ι) → k) i))
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0
hz : Eq.{u_3 + 1} (α := V) ((fun (i : ι) ↦ w i • (p i -ᵥ p i0)) i0) 0
i : ι
h : ¬i = i0
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
simp [hwdef, 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
v : V
p : ι → P
hι : IsEmpty ι
mp :
  v = 0 →
    ∃ (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 →
    ∃ (s : Finset ι) (w : ι → k), Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ v = (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]

Premises used: Submodule.mem_bot, vectorSpan_empty, Set.range_eq_empty
-- 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
hι : IsEmpty ι
h :
  ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ ∅, w i) 0 ∧
      Eq.{u_3 + 1} (α := V) (0 : V) ((Finset.weightedVSub ∅ p : (a : ι → k) → V) w : V)
⊢ ∃ (s : Finset ι) (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0 ∧ Eq.{u_3 + 1} (α := V) (0 : V) ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
use ∅
-- 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
hι : IsEmpty ι
⊢ ∃ (w : ι → k),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ ∅, w i) 0 ∧
      Eq.{u_3 + 1} (α := V) (0 : V) ((Finset.weightedVSub ∅ p : (a : ι → k) → V) w : V)

Tactic:
simp
-- 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
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
weightedVSub_mem_vectorSpan hw p

Premises used: weightedVSub_mem_vectorSpan
-- 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
s : Finset ι
w : ι → k
hw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
exact weightedVSub_mem_vectorSpan hw p

Premises used: weightedVSub_mem_vectorSpan