awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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,
      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
have 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
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]
-- 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
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 ∧
    v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
have hw : 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]
-- 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
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
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ insert i0 l.support, w i) 0 ∧
    v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
have right : v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
Tactic: use hw
-- 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
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
⊢ v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
have hz : 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 _
-- 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
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
⊢ v = ((insert i0 l.support).weightedVSub p : (a : ι → k) → V) w
have 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))
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]
-- 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
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
⊢ 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))
have 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))
Tactic: change (∑ i ∈ l.support, l i • _) = _
-- 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
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
⊢ 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))
have 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)
Tactic: congr with i
-- 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
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 : ι
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
have 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)
Tactic: by_cases h : i = i0
-- 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
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)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := k) ((l : (a : ι) → k) i : k) (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
have 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)
Tactic: by_cases h : i = i0
-- 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
v : V
p : ι → P
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
have 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
Tactic: rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
-- 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
p : ι → P
hι : IsEmpty ι
⊢ ∃ (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)
have 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)
Tactic: use ∅
-- 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
v : V
p : ι → P
⊢ 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
have 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
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
-- 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
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
⊢ 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
have 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
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
-- 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 : 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 hn : (↑(affineSpan k (Set.range p)) : Set P).Nonempty
Tactic: have hn : (affineSpan k (Set.range p) : Set P).Nonempty := ⟨p1, h⟩
-- 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 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 ι
Tactic: rw [affineSpan_nonempty, Set.range_nonempty_iff_nonempty] at hn
Cleared hypotheses: hn
-- 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
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
have 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
Tactic: obtain ⟨i0⟩ := hn
Cleared hypotheses: hn
-- 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 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) p1
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 h0 : 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)
-- 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 : 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),
    Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have hd : 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
-- 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 : 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) 1 ∧ p1 = (Finset.affineCombination k s p : (a : ι → k) → P) w
have 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
Tactic: rw [direction_affineSpan, mem_vectorSpan_iff_eq_weightedVSub] at hd
Cleared hypotheses: hd
-- 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
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
⊢ ∃ (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 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
Tactic: rcases hd with ⟨s, w, h, hs⟩
Cleared hypotheses: hd
-- 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
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0
have rw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) (∑ i ∈ s, w i)
Tactic: 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
rw : Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) (∑ i ∈ s, w i)
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s', w' i) 0
have rw₁ : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) (∑ i ∈ s, w i)
Tactic: rw [← h, Finset.sum_indicator_subset _ (Finset.subset_insert i0 s)]