awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_6
V : Type u_7
P : Type u_8
inst : CommRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_9
inst_4 : DecidableEq ι
s : Finset ι
p : ι → P
w : ι → k
i : ι
hi : i ∈ s
r : k
rw :
  Eq.{u_8 + 1} (α := P) ((AffineMap.lineMap (p i) ((affineCombination k s p : (a : ι → k) → P) w) : (a : k) → P) r : P)
    ((affineCombination k s p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i 1) w : (a : k) → (j : ι) → k) r : (j : ι) → k) :
      P)
rw₁ :
  Eq.{u_8 + 1} (α := P) ((AffineMap.lineMap (p i) ((affineCombination k s p : (a : ι → k) → P) w) : (a : k) → P) r : P)
    (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1))
              ((affineCombination k s p : (a : ι → k) → P) w) :
            k →ᵃ[k] P) :
          (a : k) → P)
        r :
      P)
rw₂ rw₃ :
  Eq.{u_8 + 1} (α := P) ((AffineMap.lineMap (p i) ((affineCombination k s p : (a : ι → k) → P) w) : (a : k) → P) r : P)
    ((AffineMap.lineMap (p i) ((affineCombination k s p : (a : ι → k) → P) w) : (a : k) → P) r : P)
⊢ Eq.{u_8 + 1} (α := P)
    ((AffineMap.homothety (p i) r : (a : P) → P) ((affineCombination k s p : (a : ι → k) → P) w : P) : P)
    ((affineCombination k s p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) i 1) w : (a : k) → (j : ι) → k) r : (j : ι) → k) :
      P)

Tactic:
rw [AffineMap.homothety_eq_lineMap, ← Finset.lineMap_affineCombination,
    Finset.affineCombination_piSingle _ _ _ hi]

Premises used: Finset.affineCombination_piSingle, Finset.lineMap_affineCombination, AffineMap.homothety_eq_lineMap
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
inl :
  ∀ (hι : IsEmpty ι),
    Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p))
      ((s.weightedVSub p : (a : ι → k) → V) w : V)
inr :
  ∀ (i0 : ι),
    Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p))
      ((s.weightedVSub p : (a : ι → k) → V) w : V)
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)

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

Tactic:
simp [Finset.eq_empty_of_isEmpty s]

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

Tactic:
rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
        Finsupp.mem_span_image_iff_linearCombination,
        Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0),
        Finset.weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply, Set.image_univ, vectorSpan_range_eq_span_range_vsub_right, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
⊢ ∀ (i : ι), w' i ≠ 0 → i ∈ s

Tactic:
have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
right :
  Eq.{u_3 + 1} (α := V)
    ((Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) (Finsupp.onFinset s w' hwx) : V)
    (∑ i ∈ s, w i • (p i -ᵥ p i0) : V)
⊢ ∃ (l : ι →₀ k),
    Membership.mem (γ := Submodule k (ι →₀ k)) (Finsupp.supported k k Set.univ) l ∧
      Eq.{u_3 + 1} (α := V) ((Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) l : V)
        (∑ i ∈ s, w i • (p i -ᵥ p i0) : V)

Tactic:
use Finsupp.onFinset s w' hwx, Set.subset_univ _

Premises used: Set.subset_univ, Finsupp.onFinset
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
right : Eq.{u_3 + 1} (α := V) (∑ a ∈ s, w' a • (p a -ᵥ p i0)) (∑ i ∈ s, w i • (p i -ᵥ p i0))
right₁ : ∀ (a : ι), HSMul.hSMul.{u_2, u_3, u_3} (α := k) 0 (p a -ᵥ p i0) = 0
⊢ Eq.{u_3 + 1} (α := V)
    ((Finsupp.linearCombination k fun (i : ι) ↦ p i -ᵥ p i0 : (a : ι →₀ k) → V) (Finsupp.onFinset s w' hwx) : V)
    (∑ i ∈ s, w i • (p i -ᵥ p i0) : V)

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.onFinset_sum hwx]

Premises used: Finsupp.onFinset_sum, Finsupp.linearCombination_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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
right : ∀ x ∈ s, w' x • (p x -ᵥ p i0) = w x • (p x -ᵥ p i0)
⊢ Eq.{u_3 + 1} (α := V) (∑ a ∈ s, w' a • (p a -ᵥ p i0)) (∑ i ∈ s, w i • (p i -ᵥ p i0))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
i : ι
hi : i ∈ s
⊢ w' i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
simp [w', Set.indicator_apply, if_pos hi]

Premises used: Set.indicator_apply, if_pos
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (a : ι), HSMul.hSMul.{u_2, u_3, u_3} (α := k) 0 (p a -ᵥ p i0) = 0

Tactic:
fun _ => zero_smul k _

Premises used: VSub.vsub, zero_smul
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
w' : (x : ι) → k := (↑s : Set ι).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (a : ι), HSMul.hSMul.{u_2, u_3, u_3} (α := k) 0 (p a -ᵥ p i0) = 0

Tactic:
exact fun _ => zero_smul k _

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

Tactic:
classical
    rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
    · simp [Finset.eq_empty_of_isEmpty s]
    · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
        Finsupp.mem_span_image_iff_linearCombination,
        Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0),
        Finset.weightedVSubOfPoint_apply]
      let w' := Set.indicator (↑s) w
      have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_zero
      use Finsupp.onFinset s w' hwx, Set.subset_univ _
      rw [Finsupp.linearCombination_apply, Finsupp.onFinset_sum hwx]
      · apply Finset.sum_congr rfl
        intro i hi
        simp [w', Set.indicator_apply, if_pos hi]
      · exact fun _ => zero_smul k _

Premises used: Finset.weightedVSubOfPoint_apply, Set.image_univ, Set.indicator_apply, Set.subset_univ, isEmpty_or_nonempty, Finsupp.linearCombination_apply, zero_smul, Finsupp.mem_span_image_iff_linearCombination, Finset.sum_congr, 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 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
⊢ Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0

Tactic:
have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
⊢ s.Nonempty

Tactic:
have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
hn : s.Nonempty
obtain :
  ∀ (i1 : ι) (hi1 : i1 ∈ s),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
obtain ⟨i1, hi1⟩ := 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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1

Tactic:
simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]

Premises used: Pi.zero_apply, Finset.sum_const_zero, Finset.sum_update_of_mem, Function.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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1

Tactic:
have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
⊢ (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1

Tactic:
have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
rw :
  Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p))
    ((s.weightedVSub p : (a : ι → k) → V) (w - w1) : V)
⊢ Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)

Tactic:
rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]

Premises used: Finset.affineCombination_vsub, direction_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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
h₁ : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, (w - w1) i) 0
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p))
    ((s.weightedVSub p : (a : ι → k) → V) (w - w1) : V)

Tactic:
apply weightedVSub_mem_vectorSpan

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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
⊢ Eq.{u_2 + 1} (α := k) (∑ i ∈ s, (w - w1) i) 0

Tactic:
simp [Pi.sub_apply, h, hw1]

Premises used: 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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
⊢ Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)

Tactic:
have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
hv :
  Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)
rw :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1) +ᵥ p i1)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
rw [← vsub_vadd (s.affineCombination k p w) (p i1)]

Premises used: Finset.affineCombination, vsub_vadd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
hv :
  Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1) +ᵥ p i1)

Tactic:
AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))

Premises used: Set.mem_range_self, mem_affineSpan, AffineSubspace.vadd_mem_of_mem_direction
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (β := fun (a : ι) ↦ k) (Function.const ι 0) i1 1
hw1 : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w1 i) 1
hw1s : (Finset.affineCombination k s p : (a : ι → k) → P) w1 = p i1
hv :
  Membership.mem (γ := Submodule k V) (AffineSubspace.direction (affineSpan k (Set.range p)))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    (((Finset.affineCombination k s p : (a : ι → k) → P) w -ᵥ p i1) +ᵥ p i1)

Tactic:
exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))

Premises used: Set.mem_range_self, mem_affineSpan, AffineSubspace.vadd_mem_of_mem_direction
-- 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
inl :
  ∀ (hs : Subsingleton k),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
inr :
  ∀ (hn : Nontrivial k),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
      ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
rcases subsingleton_or_nontrivial k with hs | hn

Premises used: subsingleton_or_nontrivial
-- 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
hs : Subsingleton k
⊢ Subsingleton V

Tactic:
have hnv := Module.subsingleton k V
-- 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
hs : Subsingleton k
hnv : Subsingleton V
⊢ Subsingleton P

Tactic:
rw [AddTorsor.subsingleton_iff V P] at hnv

Premises used: AddTorsor.subsingleton_iff
-- 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
hs : Subsingleton k
hnv : Subsingleton P
inl :
  Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P) ⊤
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (Set.range_nonempty p)]

Premises used: Iff.mpr, Set.range_nonempty, affineSpan_eq_top_iff_nonempty_of_subsingleton
-- 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
hs : Subsingleton k
hnv : Subsingleton P
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := AffineSubspace k P) ⊤
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)

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
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:
affineCombination_mem_affineSpan h p

Premises used: affineCombination_mem_affineSpan