awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k s p : (a : ι → k) → P)
        (c • weightedVSubVSubWeights k j i + Pi.single (M := fun (j : ι) ↦ k) i 1) :
      P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSub p : (a : ι → k) → V) (c • weightedVSubVSubWeights k j i) : V)
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i j c) : P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
have rw₂ : HVAdd.hVAdd (β := P) (HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V))
    ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
  (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
Tactic: rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
    weightedVSub_const_smul, s.affineCombination_piSingle k p hi,
    s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k s p : (a : ι → k) → P)
        (c • weightedVSubVSubWeights k j i + Pi.single (M := fun (j : ι) ↦ k) i 1) :
      P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSub p : (a : ι → k) → V) (c • weightedVSubVSubWeights k j i) : V)
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
rw₂ :
  HVAdd.hVAdd (β := P)
      (HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V))
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i j c) : P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
have rw₃ : HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V) +ᵥ p i =
  (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
Tactic: rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
    weightedVSub_const_smul, s.affineCombination_piSingle k p hi,
    s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k s p : (a : ι → k) → P)
        (c • weightedVSubVSubWeights k j i + Pi.single (M := fun (j : ι) ↦ k) i 1) :
      P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSub p : (a : ι → k) → V) (c • weightedVSubVSubWeights k j i) : V)
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
rw₂ :
  HVAdd.hVAdd (β := P)
      (HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V))
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
rw₃ :
  HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V) +ᵥ p i =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i j c) : P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
have rw₄ : c • (p j -ᵥ p i) +ᵥ p i = (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
Tactic: rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
    weightedVSub_const_smul, s.affineCombination_piSingle k p hi,
    s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_3 : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k s p : (a : ι → k) → P)
        (c • weightedVSubVSubWeights k j i + Pi.single (M := fun (j : ι) ↦ k) i 1) :
      P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSub p : (a : ι → k) → V) (c • weightedVSubVSubWeights k j i) : V)
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
rw₂ :
  HVAdd.hVAdd (β := P)
      (HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V))
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (j : ι) ↦ k) i 1) : P) =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
rw₃ :
  HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k j i) : V) +ᵥ p i =
    (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
rw₄ : c • (p j -ᵥ p i) +ᵥ p i = (AffineMap.lineMap (p i) (p j) : (a : k) → P) c
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i j c) : P)
    ((AffineMap.lineMap (p i) (p j) : (a : k) → P) c : P)
have rw₅ : c • (p j -ᵥ p i) +ᵥ p i = c • (p j -ᵥ p i) +ᵥ p i
Tactic: rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
    weightedVSub_const_smul, s.affineCombination_piSingle k p hi,
    s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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
⊢ 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)
have 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)
Tactic: rw [AffineMap.homothety_eq_lineMap, ← Finset.lineMap_affineCombination,
    Finset.affineCombination_piSingle _ _ _ hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AffineMap.homothety_eq_lineMap, ← Finset.lineMap_affineCombination,
    Finset.affineCombination_piSingle _ _ _ hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
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)
⊢ 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)
have 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)
Tactic: rw [AffineMap.homothety_eq_lineMap, ← Finset.lineMap_affineCombination,
    Finset.affineCombination_piSingle _ _ _ hi]
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have inl : ∀ (hι : IsEmpty ι),
  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⟩⟩)
-- 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
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)
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have inr : ∀ (i0 : ι),
  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⟩⟩)
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
i0 : ι
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have 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)
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]
-- 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
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
⊢ ∃ (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)
have hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
Tactic: have hwx : ∀ i, w' i ≠ 0 → i ∈ s := fun i => Set.mem_of_indicator_ne_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
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
⊢ ∃ (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)
have 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)
Tactic: use Finsupp.onFinset s w' hwx, Set.subset_univ _
-- 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
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
⊢ 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)
have right : Eq.{u_3 + 1} (α := V) (∑ a ∈ s, w' a • (p a -ᵥ p i0)) (∑ i ∈ s, w i • (p i -ᵥ p i0))
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.onFinset_sum hwx]
-- 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
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))
⊢ 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)
have right₁ : ∀ (a : ι), HSMul.hSMul.{u_2, u_3, u_3} (α := k) 0 (p a -ᵥ p i0) = 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.onFinset_sum hwx]
-- 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
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
⊢ Eq.{u_3 + 1} (α := V) (∑ a ∈ s, w' a • (p a -ᵥ p i0)) (∑ i ∈ s, w i • (p i -ᵥ p i0))
have right : ∀ x ∈ s, w' x • (p x -ᵥ p i0) = w x • (p x -ᵥ p i0)
Tactic: apply Finset.sum_congr rfl
-- 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
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
p : ι → P
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have inl : ∀ (hι : IsEmpty ι),
  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 _
-- 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
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)
⊢ Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p)) ((s.weightedVSub p : (a : ι → k) → V) w : V)
have inr : ∀ (i0 : ι),
  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 _
-- 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
inst_4 : Nontrivial k
s : Finset ι
w : ι → k
h : Eq.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 1
p : ι → P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hnz : Ne.{u_2 + 1} (α := k) (∑ i ∈ s, w i) 0
Tactic: have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (hypothesis)
Goal:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hn : s.Nonempty
Tactic: have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
-- 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
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have 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)
Tactic: obtain ⟨i1, hi1⟩ := 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
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hw1 : 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]
-- 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
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range p))
    ((Finset.affineCombination k s p : (a : ι → k) → P) w : P)
have hw1s : (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 ..
-- 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
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)
have rw : Membership.mem (α := V) (γ := Submodule k V) (vectorSpan k (Set.range p))
  ((s.weightedVSub p : (a : ι → k) → V) (w - w1) : V)
Tactic: rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]