awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' t)) s.centroid
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
⊢ False
have rw : ∀
  (h :
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P))
  (hssubset : t ⊂ Set.univ) (i : Fin (n + 1)) (hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t), False
Tactic: rw [s.centroid_eq_affineCombination] at h
Cleared hypotheses: h, hssubset, i, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P)
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
h₁ :
  let w : Fin (n + 1) → k := centroidWeights k univ;
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ False
have wdef : let w : Fin (n + 1) → k := centroidWeights k univ;
w = centroidWeights k univ
Tactic: set w := (centroidWeights k (univ : Finset (Fin (n + 1)))) with wdef
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
have rw : Eq.{u_1 + 1} (α := k) 1 1
Tactic: rw [sum_centroidWeights_eq_one_of_nonempty _ _ (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
⊢ False
have hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
Tactic: have hw : ∑ i, w i = 1 := by rw [sum_centroidWeights_eq_one_of_nonempty _ _ (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ False
have h1 : w i = 0
Tactic: have h1 := AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan s.independent hw h
    (by simp) hi.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h1 : w i = 0
⊢ False
have h2 : w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1
Tactic: have h2 : w i = (1 : k) / (n + 1) := by
    simp [wdef, centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h1 : w i = 0
h2 : w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1
⊢ False
have h1₁ : HAdd.hAdd (α := k) (↑n : k) 1 = 0
Tactic: simp only [h2, one_div, inv_eq_zero] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h2 : w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1
h1 : HAdd.hAdd (α := k) (↑n : k) 1 = 0
⊢ False
have norm_cast : ∀ (h1 : False), False
Tactic: norm_cast at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
⊢ s.centroid -ᵥ p = HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ p))
have rw : ∑ i : Fin (n + 1), centroidWeights k univ i • (s.points i -ᵥ p) =
  HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ p))
Tactic: rw [centroid_vsub_const _ _ (by simp), centroid_def, affineCombination_eq_linear_combination
    (hw := sum_centroidWeights_eq_one_of_nonempty _ _ (by simp))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.centroid =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) +ᵥ s.points i
have rw : s.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i
Tactic: rw [← s.centroid_vsub_eq, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
rw : s.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i
⊢ s.centroid =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) +ᵥ s.points i
have rw₁ : s.centroid = s.centroid
Tactic: rw [← s.centroid_vsub_eq, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.points i) = ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)
have rw : HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
Tactic: rw [centroid_eq_smul_sum_vsub_vadd s i, vadd_vsub, smul_smul, mul_inv_cancel₀, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0
have h : s.centroid -ᵥ s.centroid =
  HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))
Tactic: have h := centroid_vsub_eq s s.centroid
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
h :
  s.centroid -ᵥ s.centroid =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0
have h₁ : 0 = HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))
Tactic: simp only [vsub_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
h : 0 = HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0
have h₁ : HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) = 0
Tactic: symm at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
h : HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) = 0
⊢ HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
⊢ p = s.centroid ↔ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
have mp : p = s.centroid → Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
mp : p = s.centroid → Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
⊢ p = s.centroid ↔ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
have mpr : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0 → p = s.centroid
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : p = s.centroid
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
have mp : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0
Tactic: rw [h, centroid_weighted_vsub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : p = s.centroid
mp : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
have mp₁ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [h, centroid_weighted_vsub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
⊢ p = s.centroid
have mpr : p -ᵥ s.centroid = 0
Tactic: rw [← vsub_eq_zero_iff_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
have apply : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) univ x → s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
x : Fin (n + 1)
hx : Membership.mem (γ := Finset (Fin (n + 1))) univ x
⊢ s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)
have rw : s.points x -ᵥ p = s.points x -ᵥ p
Tactic: rw [vsub_sub_vsub_cancel_right _ _ s.centroid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
⊢ p -ᵥ s.centroid = 0
have this : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
  (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
Tactic: have : ∑ i, (s.points i -ᵥ p) = ∑ i, ((s.points i -ᵥ s.centroid) - (p -ᵥ s.centroid)) := by
      apply sum_congr rfl
      intro x hx
      rw [vsub_sub_vsub_cancel_right _ _ s.centroid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
⊢ p -ᵥ s.centroid = 0
have h₁ : HSub.hSub (α := V) 0 (∑ x : Fin (n + 1), (p -ᵥ s.centroid)) = 0
Tactic: rw [this, sum_sub_distrib, centroid_weighted_vsub_eq_zero] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
h : HSub.hSub (α := V) 0 (∑ x : Fin (n + 1), (p -ᵥ s.centroid)) = 0
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
⊢ p -ᵥ s.centroid = 0
have h₁ : (n + 1) • (p -ᵥ s.centroid) = 0
Tactic: simp only [sum_const, card_univ, Fintype.card_fin, zero_sub, neg_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
⊢ p -ᵥ s.centroid = 0
have h' : HAdd.hAdd (α := k) (↑n : k) 1 • (p -ᵥ s.centroid) = 0
Tactic: have h' : ((n : k) + 1) • (p -ᵥ s.centroid) = 0 := by norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : HAdd.hAdd (α := k) (↑n : k) 1 • (p -ᵥ s.centroid) = 0
⊢ HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ Finset.centroid k univ (s.face h).points = Finset.centroid k fs s.points
have h₁ : fs =
  Finset.map
    (RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
      (fs.orderEmbOfFin h))
    univ
Tactic: convert! (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ fs =
    Finset.map
      (RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
        (fs.orderEmbOfFin h))
      univ
have h₁ : (↑fs : Set (Fin (n + 1))) =
  Set.range (ι := Fin (m + 1))
    (⇑(RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
          (fs.orderEmbOfFin h)) :
      (a : Fin (m + 1)) → Fin (n + 1))
Tactic: rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
⊢ Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂
have refine : ∀ (h : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points), fs₁ = fs₂
Tactic: refine ⟨fun h => ?_, @congrArg _ _ fs₁ fs₂ (fun z => Finset.centroid k z s.points)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points
⊢ fs₁ = fs₂
have h₃ : Eq.{u_3 + 1} (α := P)
  ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
  ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
Tactic: rw [Finset.centroid_eq_affineCombination_fintype,
    Finset.centroid_eq_affineCombination_fintype] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
⊢ fs₁ = fs₂
have ha : (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₁) =
  (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₂)
Tactic: have ha :=
    (affineIndependent_iff_indicator_eq_of_affineCombination_eq k s.points).1 s.independent _ _ _ _
      (fs₁.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₁)
      (fs₂.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₂) h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
ha :
  (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₁) =
    (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₂)
⊢ fs₁ = fs₂
have ha₁ : ∀ (x : Fin (n + 1)),
  Eq.{u_1 + 1} (α := k) ((↑fs₁ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1) : k)⁻¹) x)
    ((↑fs₂ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1) : k)⁻¹) x)
Tactic: simp_rw [Finset.coe_univ, Set.indicator_univ, funext_iff,
    Finset.centroidWeightsIndicator_def, Finset.centroidWeights, h₁, h₂] at ha
Cleared hypotheses: ha