awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : CommRing k
inst_1 : NoZeroDivisors k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h_1 : Nontrivial k
w : (↑Set.univ : Type) → Fin 3 → k :=
  fun (i : (↑Set.univ : Type)) ↦
    Finset.affineCombinationLineMapWeights ((↑i : Fin 3) + 1) ((↑i : Fin 3) + 2) (r (↑i : Fin 3))
hw : ∀ (i : (↑Set.univ : Type)), Eq.{u_1 + 1} (α := k) (∑ j : Fin 3, w i j) 1
w' : Fin (HAdd.hAdd (α := ℕ) 2 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ j : Fin (2 + 1), w' j) 1
h :
  ∀ (i : (↑Set.univ : Type)),
    ∃ (r : k),
      ∀ (j : Fin (HAdd.hAdd (α := ℕ) 2 1)),
        r * Set.indicator {(↑i : Fin (2 + 1))}ᶜ (w i) j = Set.indicator {(↑i : Fin (2 + 1))}ᶜ w' j
hp' :
  ∀ (i : Fin 3),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
hp'w :
  ∀ (i : (↑Set.univ : Type)),
    Membership.mem (α := P) (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points (↑i : Fin 3))
          (singleton (α := P)
            ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) (w i) : P))))
      ((Finset.affineCombination k Finset.univ t.points : (a : Fin (2 + 1) → k) → P) w' : P)
h' :
  ∀ (i : Fin 3),
    ∃ (c : k), ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k :=
  fun (i : Fin 3) ↦
    ⋯.choose (p := fun (c : k) ↦
      ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j)
hc_1 : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr :
  HMul.hMul (α := k) (∏ i : Fin 3, c i) (∏ i : Fin 3, r i) =
    HMul.hMul (α := k) (∏ i : Fin 3, c i) (∏ i : Fin 3, (1 - r i))
hc : ¬Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, c i) 0
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i) (∏ i : Fin 3, (1 - r i))

Tactic:
exact mul_left_cancel₀ hc hcr

Premises used: mul_left_cancel₀
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      p'
rw : Ne.{u_1 + 1} (α := k) (∏ x : Fin 3, r x) 0
⊢ Eq.{u_1 + 1} (α := k) (∏ i : Fin 3, r i / (1 - r i)) 1

Tactic:
rw [Finset.prod_div_distrib, ← prod_eq_prod_one_sub_of_mem_line_point_lineMap hp', div_self]

Premises used: Affine.Triangle.prod_eq_prod_one_sub_of_mem_line_point_lineMap, Finset.prod_div_distrib, div_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      p'
⊢ Ne.{u_1 + 1} (α := k) (∏ x : Fin 3, r x) 0

Tactic:
Finset.prod_ne_zero_iff.2 fun _ _ ↦ hr0 _

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
hr0 : ∀ (i : Fin 3), r i ≠ 0
p' : P
hp' :
  ∀ (i : Fin 3),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (t.points i)
          (singleton (α := P) ((AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2)) : (a : k) → P) (r i) : P))))
      p'
⊢ Ne.{u_1 + 1} (α := k) (∏ x : Fin 3, r x) 0

Tactic:
exact Finset.prod_ne_zero_iff.2 fun _ _ ↦ hr0 _

Premises used: Iff.mpr, Finset.prod_ne_zero_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 ι
w : ι → k
p : ι → P
b : P
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p b : (a : ι → k) → V) w : V) (∑ i ∈ s, w i • (p i -ᵥ b) : V)

Tactic:
simp [weightedVSubOfPoint, LinearMap.sum_apply]

Premises used: Finset.weightedVSubOfPoint, LinearMap.sum_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 b : P
rw : ∑ i ∈ s, w i • (p -ᵥ b) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ b)
rw₁ rw₂ : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w i • (p -ᵥ b)) (∑ i ∈ s, w i • (p -ᵥ b))
⊢ (s.weightedVSubOfPoint (fun (x : ι) ↦ p) b : (a : ι → k) → V) w =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (p -ᵥ b)

Tactic:
rw [weightedVSubOfPoint_apply, sum_smul]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.sum_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 ι
w : ι → k
p : ι → P
b : P
v : V
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint (v +ᵥ p) b : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p (-v +ᵥ b) : (a : ι → k) → V) w : V)

Tactic:
simp [vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm
-- 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
G : Type u_6
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
s : Finset ι
w : ι → k
p : ι → V
b : V
a : G
⊢ (s.weightedVSubOfPoint (a • p) b : (a : ι → k) → V) w =
    HSMul.hSMul (β := V) a ((s.weightedVSubOfPoint p (a⁻¹ • b) : (a : ι → k) → V) w : V)

Tactic:
simp [smul_sum, smul_sub, smul_comm a (w _)]

Premises used: smul_sub, Finset.smul_sum, SMulCommClass.smul_comm
-- 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
b : P
simp_rw : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p₁ i -ᵥ b)) (∑ i ∈ s, w₂ i • (p₂ i -ᵥ b))
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p₁ b : (a : ι → k) → V) w₁ : V)
    ((s.weightedVSubOfPoint p₂ b : (a : ι → k) → V) w₂ : V)

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
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p₁ i -ᵥ b)) (∑ i ∈ s, w₂ i • (p₂ i -ᵥ b))

Tactic:
sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, 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₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
refine : ∀ (i : ι) (hi : i ∈ s), w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p₁ i -ᵥ b)) (∑ i ∈ s, w₂ i • (p₂ i -ᵥ b))

Tactic:
refine sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, 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₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
rw : w₂ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
rw₁ rw₂ : w₂ i • (p₂ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)

Tactic:
rw [hw i hi, 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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
simp : Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p i -ᵥ p j)) (∑ i ∈ s, w₂ i • (p i -ᵥ p j))
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w₁ : V)
    ((s.weightedVSubOfPoint p (p j) : (a : ι → k) → V) w₂ : V)

Tactic:
simp only [Finset.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
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
e_f : Eq (α := ι → V) (fun (i : ι) ↦ w₁ i • (p i -ᵥ p j)) fun (i : ι) ↦ w₂ i • (p i -ᵥ p j)
⊢ Eq.{u_2 + 1} (α := V) (∑ i ∈ s, w₁ i • (p i -ᵥ p j)) (∑ i ∈ s, w₂ i • (p i -ᵥ p j))

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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
e_f : ∀ (i : ι), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
⊢ Eq (α := ι → V) (fun (i : ι) ↦ w₁ i • (p i -ᵥ p j)) fun (i : ι) ↦ w₂ i • (p i -ᵥ p j)

Tactic:
ext 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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
e_f : ∀ (h : i = j), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
e_f₁ : ∀ (h : i ≠ j), w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

Tactic:
rcases eq_or_ne i j with h | h

Premises used: eq_or_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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i = j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

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 ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
i : ι
h : i ≠ j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

Tactic:
simp [hw i 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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
h₁ :
  HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V) =
    0
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V)
    ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V)

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
h₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))) 0
⊢ HSub.hSub (α := V) (β := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V)
      ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V) =
    0

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← sum_sub_distrib]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.sum_sub_distrib
-- 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) 0
b₁ b₂ : P
s₁ : s
f : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
b₁ b₂ : P
| s

Tactic:
· skip
-- 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) 0
b₁ b₂ : P
f : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
ext
-- 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) 0
b₁ b₂ : P
x : ι
f : w x • (b₂ -ᵥ b₁)
| w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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) 0
b₁ b₂ : P
f : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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) 0
b₁ b₂ : P
f : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
f₁ : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
· ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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) 0
b₁ b₂ : P
s₁ : s
f f₁ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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) 0
b₁ b₂ : P
h₁ : Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • (b₂ -ᵥ b₁)) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))) 0

Tactic:
conv_lhs =>
    congr
    · skip
    · ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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) 0
b₁ b₂ : P
h₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
h₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (b₂ -ᵥ b₁) = 0
h₃ h₄ : Eq.{u_2 + 1} (α := V) 0 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x ∈ s, w x • (b₂ -ᵥ b₁)) 0

Tactic:
rw [← sum_smul, h, zero_smul]

Premises used: Finset.sum_smul, zero_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 ι
w : ι → k
p : ι → P
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
b₁ b₂ : P
rw : b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSubOfPoint p b₁ : (a : ι → k) → V) w : V) b₁ =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((s.weightedVSubOfPoint p b₂ : (a : ι → k) → V) w : V) b₂

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← @vsub_eq_zero_iff_eq V,
    vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← add_sub_assoc, add_comm, add_sub_assoc, ←
    sum_sub_distrib]

Premises used: add_sub_assoc, Finset.weightedVSubOfPoint_apply, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq, add_comm, Finset.sum_sub_distrib
-- 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₁ b₂ : P
a : b₁ -ᵥ b₂
a₁ : ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
b₁ b₂ : P
| b₁ -ᵥ b₂

Tactic:
· skip
-- 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₁ b₂ : P
a : s
a₁ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

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
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
b₁ b₂ : P
| s

Tactic:
· skip
-- 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₁ b₂ : P
a : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
ext
-- 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₁ b₂ : P
x : ι
a : w x • (b₂ -ᵥ b₁)
| w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
a : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
a : ∀ (x : ι), w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
a₁ : ∀ (x : ι), w x • (b₂ -ᵥ b₁)
| fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
· ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
a : s
a₁ a₂ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
a : s
a₁ a₂ : fun (x : ι) ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
· congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
a : b₁ -ᵥ b₂
a₁ a₂ : ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))
| b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
conv_lhs : b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0

Tactic:
conv_lhs =>
    congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Premises used: smul_sub, vsub_sub_vsub_cancel_left
-- 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₁ b₂ : P
rw : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) (∑ i ∈ s, w i) (b₂ -ᵥ b₁) = 0
rw₁ : b₁ -ᵥ b₂ + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (b₂ -ᵥ b₁) = 0
rw₂ : b₁ -ᵥ b₂ + (b₂ -ᵥ b₁) = 0
rw₃ : b₁ -ᵥ b₁ = 0
rw₄ rw₅ : Eq.{u_2 + 1} (α := V) 0 0
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0

Tactic:
rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]

Premises used: Finset.sum_smul, vsub_add_vsub_cancel, one_smul, vsub_self