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
⊢ ∑ 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:
exact s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

Premises used: Finset.sum_smul_vsub_eq_weightedVSubOfPoint_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
p₂ : P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
rw :
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s p₁ : (a : ι → k) → P) w : P)
      ((affineCombination k s fun (i : ι) ↦ p₂ : (a : ι → k) → P) w : P) =
    (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
rw₁ rw₂ : (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂ = (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (affineCombination k s p₁ : (a : ι → k) → P) w -ᵥ p₂

Tactic:
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

Premises used: Finset.affineCombination_apply_const, Finset.sum_smul_vsub_eq_affineCombination_vsub
-- 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) 1
rw :
  VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k s fun (i : ι) ↦ p₁ : (a : ι → k) → P) w : P)
      ((affineCombination k s p₂ : (a : ι → k) → P) w : P) =
    p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
rw₁ rw₂ : p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w = p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (affineCombination k s p₂ : (a : ι → k) → P) w

Tactic:
rw [sum_smul_vsub_eq_affineCombination_vsub, affineCombination_apply_const _ _ _ h]

Premises used: Finset.affineCombination_apply_const, Finset.sum_smul_vsub_eq_affineCombination_vsub
-- 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
simp_rw :
  HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSub p : (a : ι → k) → V) w
⊢ VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ s₂) p : (a : ι → k) → P) w : P)
      ((affineCombination k s₂ p : (a : ι → k) → P) (-w) : P) =
    (s.weightedVSub p : (a : ι → k) → V) w

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 ι
inst_3 : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ HSub.hSub (α := V) (β := V) (((s \ s₂).weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V)
      ((s₂.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) (-w) : V) =
    (s.weightedVSub p : (a : ι → k) → V) w

Tactic:
s.weightedVSub_sdiff_sub h _ _

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

Tactic:
exact s.weightedVSub_sdiff_sub h _ _

Premises used: Finset.weightedVSub_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
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i

Tactic:
rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']

Premises used: Iff.mpr, Finset.affineCombination_sdiff_sub, Finset.sdiff_singleton_eq_erase, vsub_eq_zero_iff_eq, Finset.singleton_subset_iff, Finset.filter_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
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
e_a : p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)

Tactic:
congr
-- 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
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)

Tactic:
(affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm

Premises used: Finset.mem_singleton_self, Finset.affineCombination_of_eq_one_of_eq_zero, 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 : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
e_a : (-w) i = 1
e_a₁ : ∀ (i2 : ι), Membership.mem (γ := Finset ι) {i} i2 → i2 ≠ i → (-w) i2 = 0
⊢ p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)

Tactic:
refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm

Premises used: Finset.mem_singleton_self, Finset.affineCombination_of_eq_one_of_eq_zero, 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 : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (-w) i = 1

Tactic:
simp [hwi]
-- 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
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ ∀ (i2 : ι), Membership.mem (γ := Finset ι) {i} i2 → i2 ≠ i → (-w) i2 = 0

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 ι
w : ι → k
p : ι → P
hw : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
i : ι
inst_3 : DecidablePred fun (x : ι) ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
rw : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = 0
rw₁ : (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i = (s.weightedVSub p : (a : ι → k) → V) w
rw₂ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s \ {i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₃ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k (s.erase i) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
rw₄ rw₅ rw₆ :
  (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w -ᵥ p i =
    VSub.vsub.{u_2, u_3} (P := P) ((affineCombination k ({a ∈ s | a ≠ i}) p : (a : ι → k) → P) w : P)
      ((affineCombination k {i} p : (a : ι → k) → P) (-w) : P)
e_a : p i = (affineCombination k {i} p : (a : ι → k) → P) (-w)
e_a₁ : (-w) i = 1
e_a₂ e_a₃ : ∀ (i2 : ι), Membership.mem (γ := Finset ι) {i} i2 → i2 ≠ i → (-w) i2 = 0
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p : (a : ι → k) → P) w = p i

Tactic:
classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp

Premises used: Finset.mem_singleton_self, Finset.sdiff_singleton_eq_erase, vsub_eq_zero_iff_eq, Finset.affineCombination_of_eq_one_of_eq_zero, Finset.filter_ne', 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 : ι → k
p : ι → P
pred : ι → Prop
inst_3 : DecidablePred pred
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
              (Classical.choice ⋯) :
            (a : Subtype pred → k) → V)
          fun (i : Subtype pred) ↦ w (↑i : ι) :
        V)
      (Classical.choice ⋯) =
    (affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      ((weightedVSubOfPoint.{u_1, u_2, u_3, u_4} (P := P) (Finset.subtype pred s) (fun (i : Subtype pred) ↦ p (↑i : ι))
              (Classical.choice ⋯) :
            (a : Subtype pred → k) → V)
          fun (i : Subtype pred) ↦ w (↑i : ι) :
        V)
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯)
rw₂ rw₃ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k (Finset.subtype pred s) fun (i : Subtype pred) ↦ p (↑i : ι) : (a : Subtype pred → k) → P)
        fun (i : Subtype pred) ↦ w (↑i : ι) :
      P)
    ((affineCombination k ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)

Tactic:
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]

Premises used: Finset.affineCombination_apply, Finset.weightedVSubOfPoint_subtype_eq_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
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.weightedVSubOfPoint p (Classical.choice ⋯) : (a : ι → k) → V) w : V) (Classical.choice ⋯) =
    (affineCombination k s p : (a : ι → k) → P) w
rw₁ :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (({x ∈ s | pred x}.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 ⋯)
rw₂ 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 ({x ∈ s | pred x}) p : (a : ι → k) → P) w : P)
    ((affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
rw [affineCombination_apply, affineCombination_apply,
    s.weightedVSubOfPoint_filter_of_ne _ _ _ h]

Premises used: Finset.weightedVSubOfPoint_filter_of_ne, 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
v : V
x : k
s : Set ι
p : ι → P
b : P
simp_rw :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b : (a : ι → k) → V) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧
        v = (fs.weightedVSubOfPoint (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)) b : (a : (↑s : Type u_4) → k) → V) w

Tactic:
simp_rw [weightedVSubOfPoint_apply]

Premises used: Finset.weightedVSubOfPoint_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
v : V
x : k
s : Set ι
p : ι → P
b : P
mp :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) →
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
mpr :
  (∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) →
    ∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)
⊢ (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)

Tactic:
constructor
-- 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 : Set ι
p : ι → P
b : P
fs : Finset ι
hfs : (↑fs : Set ι) ⊆ s
w : ι → k
⊢ ∃ (fs_1 : Finset (↑s : Type u_4)) (w_1 : (↑s : Type u_4) → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ fs_1, w_1 i) (∑ i ∈ fs, w i) ∧
      Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p i -ᵥ b)) (∑ i ∈ fs_1, w_1 i • (p (↑i : ι) -ᵥ b))

Tactic:
⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).symm⟩

Premises used: Finset.sum_subtype_of_mem, Membership.mem, And.intro, Exists.intro, Finset.subtype, Eq.symm, Subtype.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
ι : Type u_4
s : Set ι
p : ι → P
b : P
fs : Finset ι
hfs : (↑fs : Set ι) ⊆ s
w : ι → k
⊢ ∃ (fs_1 : Finset (↑s : Type u_4)) (w_1 : (↑s : Type u_4) → k),
    Eq.{u_1 + 1} (α := k) (∑ i ∈ fs_1, w_1 i) (∑ i ∈ fs, w i) ∧
      Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p i -ᵥ b)) (∑ i ∈ fs_1, w_1 i • (p (↑i : ι) -ᵥ b))

Tactic:
exact ⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).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 : Set ι
p : ι → P
b : P
fs : Finset (↑s : Type u_4)
w : (↑s : Type u_4) → k
⊢ ∃ (fs_1 : Finset ι),
    (↑fs_1 : Set ι) ⊆ s ∧
      ∃ (w_1 : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs_1, w_1 i) (∑ i ∈ fs, w i) ∧
          Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) (∑ i ∈ fs_1, w_1 i • (p i -ᵥ b))

Tactic:
⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩

Premises used: Finset.map_subtype_subset, Finset.map, Membership.mem, dite, Subtype.mk, And.intro, Exists.intro, Function.Embedding.subtype, 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 : Set ι
p : ι → P
b : P
fs : Finset (↑s : Type u_4)
w : (↑s : Type u_4) → k
mpr :
  Eq.{u_1 + 1} (α := k)
    (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
      (fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i)
    (∑ i ∈ fs, w i)
mpr₁ :
  Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b))
    (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
      HSMul.hSMul.{u_1, u_2, u_2} (α := k)
        ((fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i) (p i -ᵥ b))
⊢ ∃ (fs_1 : Finset ι),
    (↑fs_1 : Set ι) ⊆ s ∧
      ∃ (w_1 : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs_1, w_1 i) (∑ i ∈ fs, w i) ∧
          Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) (∑ i ∈ fs_1, w_1 i • (p i -ᵥ b))

Tactic:
refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩
-- 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 : Set ι
p : ι → P
b : P
fs : Finset (↑s : Type u_4)
w : (↑s : Type u_4) → k
⊢ Eq.{u_1 + 1} (α := k)
    (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
      (fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i)
    (∑ i ∈ fs, w i)

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 : Set ι
p : ι → P
b : P
fs : Finset (↑s : Type u_4)
w : (↑s : Type u_4) → k
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b))
    (∑ i ∈ map (Function.Embedding.subtype fun (x : ι) ↦ x ∈ s) fs,
      HSMul.hSMul.{u_1, u_2, u_2} (α := k)
        ((fun (i : ι) ↦ (if h : i ∈ s then w (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 0 : k)) i) (p i -ᵥ b))

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
v : V
x : k
s : Set ι
p : ι → P
b : P
simp_rw :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
mp :
  (∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)) →
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)
mpr mpr₁ :
  (∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p (↑i : ι) -ᵥ b)) →
    ∃ (fs : Finset ι), (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = ∑ i ∈ fs, w i • (p i -ᵥ b)
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧ ∃ (w : ι → k), ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b : (a : ι → k) → V) w) ↔
    ∃ (fs : Finset (↑s : Type u_4)) (w : (↑s : Type u_4) → k),
      ∑ i ∈ fs, w i = x ∧
        v = (fs.weightedVSubOfPoint (fun (i : (↑s : Type u_4)) ↦ p (↑i : ι)) b : (a : (↑s : Type u_4) → k) → V) w

Tactic:
classical
    simp_rw [weightedVSubOfPoint_apply]
    constructor
    · rintro ⟨fs, hfs, w, rfl, rfl⟩
      exact ⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).symm⟩
    · rintro ⟨fs, w, rfl, rfl⟩
      refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩ <;> simp

Premises used: Finset.weightedVSubOfPoint_apply, 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
v : V
s : Set ι
p : ι → P
⊢ (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0 ∧ v = (fs.weightedVSub p : (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) 0 ∧
        v =
          (weightedVSub.{u_1, u_2, u_3, u_4} (P := P) fs fun (i : (↑s : Type u_4)) ↦ p (↑i : ι) :
              (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
simp_rw :
  (∃ (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
⊢ (∃ (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

Tactic:
simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]

Premises used: Finset.affineCombination_apply, eq_vadd_iff_vsub_eq