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
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
rw :
  HSub.hSub (α := V) (β := V) ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) s fun (i : ι) ↦ p₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
    -(s.weightedVSub p₂ : (a : ι → k) → V) w
rw₁ :
  HSub.hSub (α := V) (β := V) (0 : V) ((s.weightedVSub p₂ : (a : ι → k) → V) w : V) =
    -(s.weightedVSub p₂ : (a : ι → k) → V) w
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V)
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) : V) (-(s.weightedVSub p₂ : (a : ι → k) → V) w : V)

Tactic:
rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]

Premises used: Finset.weightedVSub_apply_const, zero_sub, Finset.sum_smul_vsub_eq_weightedVSub_sub
-- 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 ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ HAdd.hAdd (α := V) (β := V) (((s \ s₂).weightedVSub p : (a : ι → k) → V) w : V)
      ((s₂.weightedVSub p : (a : ι → k) → V) w : V) =
    (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
s.weightedVSubOfPoint_sdiff h _ _ _

Premises used: Finset.weightedVSubOfPoint_sdiff
-- 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 ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSub p : (a : ι → k) → V) w : V)
      ((s₂.weightedVSub p : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
s.weightedVSubOfPoint_sdiff_sub h _ _ _

Premises used: Finset.weightedVSubOfPoint_sdiff_sub
-- 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 : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
⊢ Eq.{u_2 + 1} (α := V)
    ((weightedVSub.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) fun (i : Subtype pred) ↦ p (↑i : ι) :
          (a : Subtype pred → k) → V)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      V)
    (({x ∈ s | pred x}.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
s.weightedVSubOfPoint_subtype_eq_filter _ _ _ _

Premises used: Finset.weightedVSubOfPoint_subtype_eq_filter, Multiset.filter
-- 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 : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
⊢ Eq.{u_2 + 1} (α := V) (({x ∈ s | pred x}.weightedVSub p : (a : ι → k) → V) w : V)
    ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
s.weightedVSubOfPoint_filter_of_ne _ _ _ h

Premises used: Finset.weightedVSubOfPoint_filter_of_ne
-- 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 : ι → k
p : ι → P
c : k
⊢ (s.weightedVSub p : (a : ι → k) → V) (c • w) = HSMul.hSMul (β := V) c ((s.weightedVSub p : (a : ι → k) → V) w : V)

Tactic:
s.weightedVSubOfPoint_const_smul _ _ _ _

Premises used: Finset.weightedVSubOfPoint_const_smul
-- 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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
simp_rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V))
      (Classical.choice ⋯)
simp_rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V))
      (Classical.choice ⋯)
simp_rw₂ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (w₂ + w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd (β := P)
      (HAdd.hAdd (α := V) (β := V) ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₂ : V)
        ((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₂ +ᵥ w₁) : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w₂ : V)
      (HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
        ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w₁ : V) (Classical.choice ⋯))

Tactic:
simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, map_add]

Premises used: vadd_vadd, map_add, vadd_eq_add, Finset.weightedVSub
-- 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 ι
p : ι → P
⊢ Eq (α := (ι → k) →ₗ[k] V) (AffineMap.linear (affineCombination k s p)) (s.weightedVSub p)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.weightedVSub, Finset.weightedVSubOfPoint, Finset.sum, rfl
-- 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 : ι → k
p : ι → P
⊢ (affineCombination k s p : (a : ι → k) → P) w =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯)

Tactic:
rfl

Premises used: rfl
-- 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 : ι → k
p : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) s (fun (x : ι) ↦ p) (Classical.choice ⋯) : (a : ι → k) → V)
          w :
        V)
      (Classical.choice ⋯) =
    p
rw₁ :
  HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯) =
    p
rw₂ : HVAdd.hVAdd (β := P) (HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p -ᵥ Classical.choice ⋯)) (Classical.choice ⋯) = p
rw₃ : HVAdd.hVAdd (β := P) (p -ᵥ Classical.choice ⋯) (Classical.choice ⋯) = p
rw₄ rw₅ : p = p
⊢ (affineCombination k s fun (x : ι) ↦ p : (a : ι → k) → P) w = p

Tactic:
rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]

Premises used: Finset.affineCombination_apply, one_smul, Finset.weightedVSubOfPoint_apply_const, vsub_vadd
-- 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
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
simp_rw :
  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 ⋯)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p₁ : (a : ι → k) → P) w₁ : P)
    ((affineCombination k s p₂ : (a : ι → k) → P) w₂ : P)

Tactic:
simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]

Premises used: Finset.weightedVSubOfPoint_congr, Finset.affineCombination_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 ι
w : ι → k
p : ι → P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
b : P
⊢ (affineCombination k s p : (a : ι → k) → P) w =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) b

Tactic:
s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w p h _ _

Premises used: Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one
-- 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
p : ι → P
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ +ᵥ w₂)
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
rw₂ rw₃ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P) ((s.weightedVSub p : (a : ι → k) → V) w₁ : V)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (affineCombination k s p : (a : ι → k) → P) (w₁ + w₂)

Tactic:
rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]

Premises used: AffineMap.map_vadd, Finset.affineCombination_linear, vadd_eq_add
-- 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
p : ι → P
rw :
  Eq.{u_2 + 1} (α := V) ((AffineMap.linear (affineCombination k s p) : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
    ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
rw₁ :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (w₁ -ᵥ w₂) : V)
    ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
    ((s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂) : V)
⊢ VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k s p : (a : ι → k) → P) w₂ : P) =
    (s.weightedVSub p : (a : ι → k) → V) (w₁ - w₂)

Tactic:
rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]

Premises used: AffineMap.linearMap_vsub, Finset.affineCombination_linear, vsub_eq_sub
-- 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
inst_3 : DecidableEq P
s : Finset P
w : P → k
f : ↥s → P
hf : Function.Injective f
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s.attach f : (a : ↥s → k) → P) (w ∘ f) : P)
    ((affineCombination k (image f univ) id : (a : P → k) → P) w : P)

Tactic:
simp [affineCombination, hf]

Premises used: Finset.affineCombination
-- 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
s : Finset P
w : P → k
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
rw₁ :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (Subtype.val (p := fun (x : P) ↦ x ∈ s)) s.attach) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)

Tactic:
rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]

Premises used: Subtype.coe_injective, Finset.univ_eq_attach, Finset.attach_affineCombination_of_injective, Subtype.val, Finset.attach_image_val
-- 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
s : Finset P
w : P → k
classical :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (α := ↥s) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) univ) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
classical₁ :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k (image (Subtype.val (p := fun (x : P) ↦ x ∈ s)) s.attach) id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
classical₂ classical₃ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s id : (a : P → k) → P) w : P)
    ((affineCombination k s id : (a : P → k) → P) w : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (w ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
    ((affineCombination k s id : (a : P → k) → P) w : P)

Tactic:
classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]

Premises used: Finset.univ_eq_attach, Finset.attach_image_val
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_6
s : Finset ι
w : ι → k
p : ι → V
hw : s.sum w = 0
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (∑ i ∈ s, w i • p i : V)

Tactic:
simp [s.weightedVSub_apply, vsub_eq_sub, smul_sub, ← Finset.sum_smul, hw]

Premises used: Finset.sum_smul, smul_sub, Finset.weightedVSub_apply, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Combination
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
ι : Type u_4
s : Finset ι
p : ι → V
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ Eq.{u_2 + 1} (α := V) ((affineCombination k s p : (a : ι → k) → V) w : V) (∑ i ∈ s, w i • p i : V)

Tactic:
simp [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw 0]

Premises used: Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, OfNat.ofNat
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1

Tactic:
have h1 : ∑ i ∈ s, w i = 1 := hwi ▸ sum_eq_single i hw0 fun h => False.elim (h his)
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) (p i) = p i
⊢ (affineCombination k s p : (a : ι → k) → P) w = p i

Tactic:
rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p h1 (p i),
    weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) 0 (p i) = p i

Tactic:
zero_vadd V (p i)

Premises used: zero_vadd
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
h : Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) 0
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) (p i) = p i

Tactic:
convert! zero_vadd V (p i)

Premises used: zero_vadd
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) 0

Tactic:
sum_eq_zero ?_

Premises used: Finset.sum_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 ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
h : ∀ x ∈ s, w x • (p x -ᵥ p i) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)) 0

Tactic:
refine sum_eq_zero ?_

Premises used: Finset.sum_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 ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i2 : ι
hi2 : i2 ∈ s
pos : ∀ (h : i2 = i), w i2 • (p i2 -ᵥ p i) = 0
neg : ∀ (h : ¬i2 = i), w i2 • (p i2 -ᵥ p i) = 0
⊢ w i2 • (p i2 -ᵥ p i) = 0

Tactic:
by_cases h : i2 = i
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i2 : ι
hi2 : i2 ∈ s
h : i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0

Tactic:
simp [h]
-- 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 : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i2 : ι
hi2 : i2 ∈ s
h : ¬i2 = i
⊢ w i2 • (p i2 -ᵥ p i) = 0

Tactic:
simp [hw0 i2 hi2 h]
-- 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
w : ι → k
p : ι → P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₁.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    (affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w)
rw₁ :
  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) ((↑s₁ : Set ι).indicator w) : V)
      (Classical.choice ⋯)
rw₂ rw₃ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₂.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((s₂.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) ((↑s₁ : Set ι).indicator w) : V)
      (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s₁ p : (a : ι → k) → P) w : P)
    ((affineCombination k s₂ p : (a : ι → k) → P) ((↑s₁ : Set ι).indicator w) : P)

Tactic:
rw [affineCombination_apply, affineCombination_apply,
    weightedVSubOfPoint_indicator_subset _ _ _ h]

Premises used: Finset.weightedVSubOfPoint_indicator_subset, Finset.affineCombination_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
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
simp_rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (((map e 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 ∘ (⇑e : (a : ι₂) → ι)) (Classical.choice ⋯) : (a : ι₂ → k) → V)
          (w ∘ (⇑e : (a : ι₂) → ι)) :
        V)
      (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) w : P)
    ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) (w ∘ (⇑e : (a : ι₂) → ι)) : P)

Tactic:
simp_rw [affineCombination_apply, weightedVSubOfPoint_map]

Premises used: Finset.weightedVSubOfPoint_map, Finset.affineCombination_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 ι
w : ι → k
p₁ p₂ : ι → P
simp_rw :
  ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ (Classical.choice ⋯) : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ (Classical.choice ⋯) : (a : ι → k) → V) w : V)
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p₁ : (a : ι → k) → P) w : P)
      ((affineCombination k s p₂ : (a : ι → k) → P) w : P)

Tactic:
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]

Premises used: vadd_vsub_vadd_cancel_right, Finset.affineCombination_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 ι
w : ι → k
p₁ p₂ : ι → P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) =
    HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p₁ (Classical.choice ⋯) : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p₂ (Classical.choice ⋯) : (a : ι → k) → V) w : V)

Tactic:
s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

Premises used: Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub