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
p0 : P
s : Set ι
p : ι → P
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p0 = (affineCombination k fs p : (a : ι → k) → P) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
        p0 = (affineCombination k fs fun (i : (↑s : Type u_4)) ↦ p (↑i : ι) : (a : (↑s : Type u_4) → k) → P) w
have simp_rw : (∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          p0 -ᵥ Classical.choice sorry = (fs.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w) ↔
  ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
      p0 -ᵥ Classical.choice sorry =
        (weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) fs (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι))
              (Classical.choice sorry) :
            (a : (↑s : Type u_4) → k) → V)
          w
Tactic: simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]
-- 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 ι
V₂ : Type u_6
P₂ : Type u_7
inst_3 : AddCommGroup V₂
inst_4 : Module k V₂
inst_5 : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
⊢ Eq.{u_7 + 1} (α := P₂) ((f : (a : P) → P₂) ((affineCombination k s p : (a : ι → k) → P) w : P) : P₂)
    ((affineCombination k s ((⇑f : (a : P) → P₂) ∘ p) : (a : ι → k) → P₂) w : P₂)
have have : ∀ (b : P),
  Eq.{u_7 + 1} (α := P₂) ((f : (a : P) → P₂) ((affineCombination k s p : (a : ι → k) → P) w : P) : P₂)
    ((affineCombination k s ((⇑f : (a : P) → P₂) ∘ p) : (a : ι → k) → P₂) w : P₂)
Tactic: have b := Classical.choice (inferInstance : AffineSpace V P).nonempty
-- 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 ι
V₂ : Type u_6
P₂ : Type u_7
inst_3 : AddCommGroup V₂
inst_4 : Module k V₂
inst_5 : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
b : P
⊢ Eq.{u_7 + 1} (α := P₂) ((f : (a : P) → P₂) ((affineCombination k s p : (a : ι → k) → P) w : P) : P₂)
    ((affineCombination k s ((⇑f : (a : P) → P₂) ∘ p) : (a : ι → k) → P₂) w : P₂)
have have : ∀ (b₂ : P₂),
  Eq.{u_7 + 1} (α := P₂) ((f : (a : P) → P₂) ((affineCombination k s p : (a : ι → k) → P) w : P) : P₂)
    ((affineCombination k s ((⇑f : (a : P) → P₂) ∘ p) : (a : ι → k) → P₂) w : P₂)
Tactic: have b₂ := Classical.choice (inferInstance : AffineSpace V₂ P₂).nonempty
-- 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 ι
V₂ : Type u_6
P₂ : Type u_7
inst_3 : AddCommGroup V₂
inst_4 : Module k V₂
inst_5 : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ Eq.{u_7 + 1} (α := P₂) ((f : (a : P) → P₂) ((affineCombination k s p : (a : ι → k) → P) w : P) : P₂)
    ((affineCombination k s ((⇑f : (a : P) → P₂) ∘ p) : (a : ι → k) → P₂) w : P₂)
have rw : (f : (a : P) → P₂) (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) b) =
  HVAdd.hVAdd.{u_6, u_7, u_7} (α := V₂) (β := P₂)
    ((weightedVSubOfPoint.{u_1, u_6, u_7, u_4} (P := P₂) s ((⇑f : (a : P) → P₂) ∘ p : ι → P₂)
            ((f : (a : P) → P₂) b : P₂) :
          (a : ι → k) → V₂)
        w :
      V₂)
    ((f : (a : P) → P₂) b : P₂)
Tactic: rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw b,
    s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w (f ∘ p) hw b₂, ←
    s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂]
-- 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 ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w : P)
    ((AffineMap.lineMap p₁ p₂ : (a : k) → P) (∑ i ∈ s ∩ s', w i) : P)
have rw : HAdd.hAdd (α := V) (∑ x ∈ s ∩ s', w x • (p x -ᵥ p₁)) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) = ∑ i ∈ s ∩ s', w i • (p₂ -ᵥ p₁)
Tactic: rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h p₁,
    weightedVSubOfPoint_apply, ← s.sum_inter_add_sum_diff s', AffineMap.lineMap_apply,
    vadd_right_cancel_iff, sum_smul]
-- 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 ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ HAdd.hAdd (α := V) (∑ x ∈ s ∩ s', w x • (p x -ᵥ p₁)) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) =
    ∑ i ∈ s ∩ s', w i • (p₂ -ᵥ p₁)
have h₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) 0
Tactic: convert! add_zero _ with i hi
-- 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 ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
h₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) 0
⊢ HAdd.hAdd (α := V) (∑ x ∈ s ∩ s', w x • (p x -ᵥ p₁)) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) =
    ∑ i ∈ s ∩ s', w i • (p₂ -ᵥ p₁)
have h₂ : ∀ (i : ι) (hi : i ∈ s ∩ s'), p₂ = p i
Tactic: convert! add_zero _ with i hi
-- 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 ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) 0
have h₁ : ∀ (i : ι) (hi : i ∈ s \ s'), w i • (p i -ᵥ p₁) = 0
Tactic: convert! Finset.sum_const_zero with i hi
-- 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 ι
w₁ w₂ : ι → k
r : k
p : ι → P
⊢ Eq.{u_3 + 1} (α := P)
    (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
              ((affineCombination k s p : (a : ι → k) → P) w₂) :
            k →ᵃ[k] P) :
          (a : k) → P)
        r :
      P)
    ((affineCombination k s p : (a : ι → k) → P) ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) : P)
have simp_rw : (AffineMap.lineMap
        (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
          ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁ : V) (Classical.choice sorry))
        (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
          ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₂ : V) (Classical.choice sorry)) :
      (a : k) → P)
    r =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V)
        ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
      V)
    (Classical.choice sorry)
Tactic: simp_rw [Finset.affineCombination_apply, ← AffineMap.lineMap_vadd, AffineMap.lineMap_apply_module,
    map_add, map_smul]
-- 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 ι
w₁ w₂ : ι → k
r : k
p : ι → P
simp_rw :
  (AffineMap.lineMap
          (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
            ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))
          (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
            ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V) (Classical.choice ⋯)) :
        (a : k) → P)
      r =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V)
          ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
        V)
      (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P)
    (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
              ((affineCombination k s p : (a : ι → k) → P) w₂) :
            k →ᵃ[k] P) :
          (a : k) → P)
        r :
      P)
    ((affineCombination k s p : (a : ι → k) → P) ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) : P)
have simp_rw₁ : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    (((AffineMap.lineMap ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁)
              ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₂) :
            k →ᵃ[k] V) :
          (a : k) → V)
        r :
      V)
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V)
        ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
      V)
    (Classical.choice sorry)
Tactic: simp_rw [Finset.affineCombination_apply, ← AffineMap.lineMap_vadd, AffineMap.lineMap_apply_module,
    map_add, map_smul]
-- 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 ι
w₁ w₂ : ι → k
r : k
p : ι → P
simp_rw :
  (AffineMap.lineMap
          (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
            ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))
          (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
            ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V) (Classical.choice ⋯)) :
        (a : k) → P)
      r =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V)
          ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
        V)
      (Classical.choice ⋯)
simp_rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (((AffineMap.lineMap ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁)
                ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂) :
              k →ᵃ[k] V) :
            (a : k) → V)
          r :
        V)
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V)
          ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
        V)
      (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P)
    (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
              ((affineCombination k s p : (a : ι → k) → P) w₂) :
            k →ᵃ[k] P) :
          (a : k) → P)
        r :
      P)
    ((affineCombination k s p : (a : ι → k) → P) ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) : P)
have simp_rw₂ : HVAdd.hVAdd (β := P)
    (HSMul.hSMul (β := V) (1 - r) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁ : V) +
      HSMul.hSMul (β := V) r ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₂ : V))
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
    ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) ((1 - r) • w₁ + r • w₂) : V) (Classical.choice sorry)
Tactic: simp_rw [Finset.affineCombination_apply, ← AffineMap.lineMap_vadd, AffineMap.lineMap_apply_module,
    map_add, map_smul]
-- 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 ι
w₁ w₂ : ι → k
r : k
p : ι → P
simp_rw :
  (AffineMap.lineMap
          (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
            ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))
          (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
            ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V) (Classical.choice ⋯)) :
        (a : k) → P)
      r =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V)
          ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
        V)
      (Classical.choice ⋯)
simp_rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (((AffineMap.lineMap ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁)
                ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂) :
              k →ᵃ[k] V) :
            (a : k) → V)
          r :
        V)
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V)
          ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) :
        V)
      (Classical.choice ⋯)
simp_rw₂ :
  HVAdd.hVAdd (β := P)
      (HSMul.hSMul (β := V) (1 - r) ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) +
        HSMul.hSMul (β := V) r ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V))
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) ((1 - r) • w₁ + r • w₂) : V)
      (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P)
    (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
              ((affineCombination k s p : (a : ι → k) → P) w₂) :
            k →ᵃ[k] P) :
          (a : k) → P)
        r :
      P)
    ((affineCombination k s p : (a : ι → k) → P) ((AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) r : ι → k) : P)
have simp_rw₃ : HVAdd.hVAdd (β := P)
    (HSMul.hSMul (β := V) (1 - r) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₁ : V) +
      HSMul.hSMul (β := V) r ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) w₂ : V))
    (Classical.choice sorry) =
  HVAdd.hVAdd (β := P)
    (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) ((1 - r) • w₁) : V)
      ((s.weightedVSubOfPoint p (Classical.choice sorry) : (a : ι → k) → V) (r • w₂) : V))
    (Classical.choice sorry)
Tactic: simp_rw [Finset.affineCombination_apply, ← AffineMap.lineMap_vadd, AffineMap.lineMap_apply_module,
    map_add, map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i : ι
h : i ∈ s
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, affineCombinationSingleWeights k i j) 1
have rw : Eq.{u_1 + 1} (α := k) (∑ j ∈ s, Pi.single (M := fun (a : ι) ↦ k) i 1 j) 1
Tactic: rw [affineCombinationSingleWeights, s.sum_pi_single', if_pos h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i : ι
h : i ∈ s
rw : Eq.{u_1 + 1} (α := k) (∑ j ∈ s, Pi.single (M := fun (a : ι) ↦ k) i 1 j) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, affineCombinationSingleWeights k i j) 1
have rw₁ : Eq.{u_1 + 1} (α := k) (if i ∈ s then 1 else 0) 1
Tactic: rw [affineCombinationSingleWeights, s.sum_pi_single', if_pos h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i : ι
h : i ∈ s
rw : Eq.{u_1 + 1} (α := k) (∑ j ∈ s, Pi.single (M := fun (a : ι) ↦ k) i 1 j) 1
rw₁ : Eq.{u_1 + 1} (α := k) (if i ∈ s then 1 else 0) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, affineCombinationSingleWeights k i j) 1
have rw₂ : Eq.{u_1 + 1} (α := k) 1 1
Tactic: rw [affineCombinationSingleWeights, s.sum_pi_single', if_pos h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ s, weightedVSubVSubWeights k i j t) 0
have simp_rw : HSub.hSub (α := k) (∑ x ∈ s, Pi.single (M := fun (a : ι) ↦ k) i 1 x) (∑ x ∈ s, Pi.single (M := fun (a : ι) ↦ k) j 1 x) =
  0
Tactic: simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ s, affineCombinationLineMapWeights i j c t) 1
have simp_rw : HAdd.hAdd (α := k) (∑ x ∈ s, (c • weightedVSubVSubWeights k j i) x) (∑ x ∈ s, Pi.single (M := fun (j : ι) ↦ k) i 1 x) =
  1
Tactic: simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
-- 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 : ι
hi : i ∈ s
⊢ (affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i 1) = p i
have refine : ∀ i2 ∈ s, i2 ≠ i → Eq.{u_1 + 1} (α := k) (Pi.single (M := fun (a : ι) ↦ k) i 1 i2 : k) (0 : k)
Tactic: refine s.affineCombination_of_eq_one_of_eq_zero _ _ hi (by simp) ?_
-- 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
⊢ (s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
have rw : (s.weightedVSub p : (a : ι → k) → V)
    (HSub.hSub (α := (j : ι) → k) (Pi.single (M := fun (a : ι) ↦ k) i 1) (Pi.single (M := fun (a : ι) ↦ k) j 1)) =
  p i -ᵥ p j
Tactic: rw [weightedVSubVSubWeights, ← affineCombination_vsub,
    s.affineCombination_piSingle k p hi, s.affineCombination_piSingle k p hj]
-- 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
rw :
  (s.weightedVSub p : (a : ι → k) → V)
      (HSub.hSub (α := (j : ι) → k) (Pi.single (M := fun (a : ι) ↦ k) i 1) (Pi.single (M := fun (a : ι) ↦ k) j 1)) =
    p i -ᵥ p j
⊢ (s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
have rw₁ : VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i 1) : P)
    ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) j 1) : P) =
  p i -ᵥ p j
Tactic: rw [weightedVSubVSubWeights, ← affineCombination_vsub,
    s.affineCombination_piSingle k p hi, s.affineCombination_piSingle k p hj]
-- 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
rw :
  (s.weightedVSub p : (a : ι → k) → V)
      (HSub.hSub (α := (j : ι) → k) (Pi.single (M := fun (a : ι) ↦ k) i 1) (Pi.single (M := fun (a : ι) ↦ k) j 1)) =
    p i -ᵥ p j
rw₁ :
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i 1) : P)
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) j 1) : P) =
    p i -ᵥ p j
⊢ (s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
have rw₂ : p i -ᵥ (affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) j 1) = p i -ᵥ p j
Tactic: rw [weightedVSubVSubWeights, ← affineCombination_vsub,
    s.affineCombination_piSingle k p hi, s.affineCombination_piSingle k p hj]
-- 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
rw :
  (s.weightedVSub p : (a : ι → k) → V)
      (HSub.hSub (α := (j : ι) → k) (Pi.single (M := fun (a : ι) ↦ k) i 1) (Pi.single (M := fun (a : ι) ↦ k) j 1)) =
    p i -ᵥ p j
rw₁ :
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i 1) : P)
      ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) j 1) : P) =
    p i -ᵥ p j
rw₂ : p i -ᵥ (affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) j 1) = p i -ᵥ p j
⊢ (s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k i j) = p i -ᵥ p j
have rw₃ : p i -ᵥ p j = p i -ᵥ p j
Tactic: rw [weightedVSubVSubWeights, ← affineCombination_vsub,
    s.affineCombination_piSingle k p hi, s.affineCombination_piSingle k p hj]
-- 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
⊢ 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 : 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)
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)
⊢ 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.{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
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]