awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯) : (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 ⋯ =
          (weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) fs (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι))
                (Classical.choice ⋯) :
              (a : (↑s : Type u_4) → k) → V)
            w

Tactic:
eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype

Premises used: Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 -ᵥ Classical.choice ⋯ = (fs.weightedVSubOfPoint p (Classical.choice ⋯) : (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 ⋯ =
          (weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) fs (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι))
                (Classical.choice ⋯) :
              (a : (↑s : Type u_4) → k) → V)
            w

Tactic:
exact eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype

Premises used: Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₂
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₂)
⊢ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
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₂)
⊢ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₂
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₂)
⊢ 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:
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₂]

Premises used: Function.comp, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₂
⊢ (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:
simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd, map_smulₛₗ,
    AffineMap.linearMap_vsub, map_sum, Function.comp_apply]

Premises used: Finset.weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.linearMap_vsub, MulActionSemiHomClass.map_smulₛₗ, AffineMap.map_vadd, map_sum, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁
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₁)
⊢ 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)

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]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.sum_smul, Finset.sum_inter_add_sum_diff, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, AffineMap.lineMap_apply, vadd_right_cancel_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁)) 0 = ∑ x ∈ s ∩ s', w x • (p x -ᵥ p₁)

Tactic:
add_zero _

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
h₂ : ∀ (i : ι) (hi : i ∈ s ∩ s'), p₂ = p i
⊢ 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:
convert! add_zero _ with i hi

Premises used: add_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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', 0) 0

Tactic:
Finset.sum_const_zero

Premises used: Finset.sum_const_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁ : ∀ (i : ι) (hi : i ∈ s \ s'), w i • (p i -ᵥ p₁) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s \ s', w x • (p x -ᵥ p₁)) 0

Tactic:
convert! Finset.sum_const_zero with i hi

Premises used: Finset.sum_const_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁
i : ι
hi : i ∈ s \ s'
⊢ w i • (p i -ᵥ p₁) = 0

Tactic:
simp [hp₁ i hi]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁
i : ι
hi : i ∈ s ∩ s'
⊢ p₂ = p i

Tactic:
(hp₂ i hi).symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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₁
i : ι
hi : i ∈ s ∩ s'
⊢ p₂ = p i

Tactic:
exact (hp₂ i hi).symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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 ⋯)
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 (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) ((1 - r) • w₁) : V)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (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)

Tactic:
simp_rw [Finset.affineCombination_apply, ← AffineMap.lineMap_vadd, AffineMap.lineMap_apply_module,
    map_add, map_smul]

Premises used: AffineMap.lineMap_apply_module, map_add, Finset.affineCombination_apply, AffineMap.lineMap_vadd, map_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i : ι
⊢ affineCombinationSingleWeights k i i = 1

Tactic:
Pi.single_eq_same _ _

Premises used: Finset.affineCombinationSingleWeights, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j : ι
h : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0

Tactic:
Pi.single_eq_of_ne h _

Premises used: Finset.affineCombinationSingleWeights, Pi.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := k) 1 1
⊢ Eq.{u_1 + 1} (α := k) (∑ j ∈ s, affineCombinationSingleWeights k i j) 1

Tactic:
rw [affineCombinationSingleWeights, s.sum_pi_single', if_pos h]

Premises used: Finset.affineCombinationSingleWeights, if_pos, Finset.sum_pi_single'
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i : ι
⊢ weightedVSubVSubWeights k i i = 0

Tactic:
simp [weightedVSubVSubWeights]

Premises used: Finset.weightedVSubVSubWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j i = 1

Tactic:
simp [weightedVSubVSubWeights, h]

Premises used: Finset.weightedVSubVSubWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j : ι
h : i ≠ j
⊢ weightedVSubVSubWeights k i j j = -1

Tactic:
simp [weightedVSubVSubWeights, h.symm]

Premises used: Finset.weightedVSubVSubWeights, Ne.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
⊢ weightedVSubVSubWeights k i j t = 0

Tactic:
simp [weightedVSubVSubWeights, hi, hj]

Premises used: Finset.weightedVSubVSubWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
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
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ s, weightedVSubVSubWeights k i j t) 0

Tactic:
simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]

Premises used: Finset.weightedVSubVSubWeights, Finset.sum_sub_distrib, Pi.sub_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
s : Finset ι
inst_1 : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ 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 [hi, hj]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i : ι
c : k
⊢ affineCombinationLineMapWeights i i c = Pi.single (M := fun (j : ι) ↦ k) i 1

Tactic:
simp [affineCombinationLineMapWeights]

Premises used: Finset.affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c i = 1 - c

Tactic:
simp [affineCombinationLineMapWeights, h.symm, sub_eq_neg_add]

Premises used: sub_eq_neg_add, Ne.symm, Finset.affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c j = c

Tactic:
simp [affineCombinationLineMapWeights, h.symm]

Premises used: Ne.symm, Finset.affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
inst : Ring k
ι : Type u_4
inst_1 : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c t = 0

Tactic:
simp [affineCombinationLineMapWeights, hi, hj]

Premises used: Finset.affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
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
⊢ Eq.{u_1 + 1} (α := k) (∑ t ∈ s, affineCombinationLineMapWeights i j c t) 1

Tactic:
simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]

Premises used: Finset.sum_add_distrib, Pi.add_apply, Finset.affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
⊢ 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 [hi, hj, ← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
⊢ Eq.{u_1 + 1} (α := k) (Pi.single (M := fun (a : ι) ↦ k) i 1 i : k) (1 : k)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
refine : ∀ i2 ∈ s, i2 ≠ i → Eq.{u_1 + 1} (α := k) (Pi.single (M := fun (a : ι) ↦ k) i 1 i2 : k) (0 : k)
⊢ (affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i 1) = p i

Tactic:
refine s.affineCombination_of_eq_one_of_eq_zero _ _ hi (by simp) ?_

Premises used: Finset.affineCombination_of_eq_one_of_eq_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
j : ι
hj : j ≠ i
⊢ Eq.{u_1 + 1} (α := k) (Pi.single (M := fun (a : ι) ↦ k) i 1 j : k) (0 : k)

Tactic:
simp [hj]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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) (affineCombinationSingleWeights k i) = p i

Tactic:
affineCombination_piSingle _ _ _ hi

Premises used: Finset.affineCombinationSingleWeights, Finset.affineCombination_piSingle
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
rw₃ rw₄ : p i -ᵥ p j = p i -ᵥ p j
⊢ (s.weightedVSub p : (a : ι → k) → V) (weightedVSubVSubWeights k i j) = p i -ᵥ p j

Tactic:
rw [weightedVSubVSubWeights, ← affineCombination_vsub,
    s.affineCombination_piSingle k p hi, s.affineCombination_piSingle k p hj]

Premises used: Finset.affineCombination_vsub, Finset.weightedVSubVSubWeights, Finset.affineCombination_piSingle
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
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
rw₅ rw₆ : c • (p j -ᵥ p i) +ᵥ p i = c • (p j -ᵥ p i) +ᵥ p i
⊢ 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)

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]

Premises used: Finset.weightedVSub_weightedVSubVSubWeights, Finset.weightedVSub_const_smul, AffineMap.lineMap_apply, Finset.affineCombinationLineMapWeights, Finset.weightedVSub_vadd_affineCombination, Finset.affineCombination_piSingle