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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
rw :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
        ((weightedVSubOfPoint {i}ᶜ s.points (s.points i) : (a : Fin (n + 1) → k) → V) fun (x : Fin (n + 1)) ↦
            (↑n : k)⁻¹ :
          V)
        (s.points i) -ᵥ
      s.points i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
⊢ s.faceOppositeCentroid i -ᵥ s.points i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have rw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ {i}ᶜ, (↑n : k)⁻¹) 1
Tactic: rw [faceOppositeCentroid_eq_affineCombination,
    affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ ?_ (s.points i)]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
        ((weightedVSubOfPoint {i}ᶜ s.points (s.points i) : (a : Fin (n + 1) → k) → V) fun (x : Fin (n + 1)) ↦
            (↑n : k)⁻¹ :
          V)
        (s.points i) -ᵥ
      s.points i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have simp : ∑ i_1 ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i_1 -ᵥ s.points i) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
Tactic: simp only [weightedVSubOfPoint_apply, vadd_vsub]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i_1 i : Fin (n + 1)
⊢ Eq.{u_2 + 1} (α := V) (∑ j ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
    (∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
have rw : ∑ j ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) =
  HAdd.hAdd (α := V) (∑ i_2 ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i_2 -ᵥ s.points i))
    (∑ i_2 ∈ {i}, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i_2 -ᵥ s.points i))
Tactic: rw [← Finset.sum_compl_add_sum {i}]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ ∑ i_1 ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i_1 -ᵥ s.points i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have h : ∀ (i : Fin (n + 1)),
  Eq.{u_2 + 1} (α := V) (∑ j ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
    (∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
Tactic: have h (i : Fin (n + 1)) : ∑ j ∈ {i}ᶜ, (n : k)⁻¹ • (s.points j -ᵥ s.points i) =
      ∑ j : (Fin (n + 1)), ((n : k)⁻¹ • (s.points j -ᵥ s.points i)) := by
      rw [← Finset.sum_compl_add_sum {i}]
      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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ j ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
      (∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
⊢ ∑ i_1 ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i_1 -ᵥ s.points i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have rw : ∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
Tactic: rw [h i, smul_sum]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ j ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
      (∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
rw :
  ∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
⊢ ∑ i_1 ∈ {i}ᶜ, HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i_1 -ᵥ s.points i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have rw₁ : Eq.{u_2 + 1} (α := V) (∑ j : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i))
  (∑ x : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points x -ᵥ s.points i))
Tactic: rw [h i, smul_sum]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ {i}ᶜ, (↑n : k)⁻¹) 1
have simp : HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ = 1
Tactic: simp only [sum_const, card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right,
      nsmul_eq_mul]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ = 1
have rw : Eq.{u_1 + 1} (α := k) 1 1
Tactic: rw [mul_inv_cancel₀ (NeZero.ne (n : k))]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) +ᵥ
      s.points i
have rw : s.faceOppositeCentroid i = (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
Tactic: rw [← faceOppositeCentroid_vsub_point_eq_smul_sum_vsub s i, 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
rw : s.faceOppositeCentroid i = (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
⊢ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) +ᵥ
      s.points i
have rw₁ : s.faceOppositeCentroid i = s.faceOppositeCentroid i
Tactic: rw [← faceOppositeCentroid_vsub_point_eq_smul_sum_vsub s i, 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i -ᵥ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points i -ᵥ s.points x))
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹
    (∑ x : Fin (n + 1), HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points x -ᵥ s.points i)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points i -ᵥ s.points x))
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, ← neg_smul,
    Lean.Grind.Ring.neg_eq_mul_neg_one, ← smul_smul, smul_sum]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.points i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.points i)
have rw : HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.points i) = ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)
Tactic: rw [smul_faceOppositeCentroid_vsub_point_eq_sum_vsub s i,
    smul_centroid_vsub_point_eq_sum_vsub s i]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
rw : HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.points i) = ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)
⊢ HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.points i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.points i)
have rw₁ : Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
Tactic: rw [smul_faceOppositeCentroid_vsub_point_eq_sum_vsub s i,
    smul_centroid_vsub_point_eq_sum_vsub s i]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
⊢ s.faceOppositeCentroid i -ᵥ s.faceOppositeCentroid j =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) -
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points j)) +
    (s.points i -ᵥ s.points j) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
Tactic: rw [faceOppositeCentroid_eq_sum_vsub_vadd s i, faceOppositeCentroid_eq_sum_vsub_vadd s j,
    vadd_vsub_vadd_comm _ _ (s.points i) (s.points j)]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i_1 j i : Fin (n + 1)
⊢ Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
    (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
have apply : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) univ x →
    s.points x -ᵥ s.points i = s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)
Tactic: apply sum_congr rfl
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) -
        HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points j)) +
      (s.points i -ᵥ s.points j) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
have h1 : ∀ (i : Fin (n + 1)),
  Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
    (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
Tactic: have h1 (i : Fin (n + 1)) : ∑ x, (s.points x -ᵥ s.points i) =
      ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)) := by
    apply sum_congr rfl
    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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) -
        HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points j)) +
      (s.points i -ᵥ s.points j) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
have simp_rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSub.hSub (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0))
          (∑ x : Fin (n + 1), (s.points i -ᵥ s.points 0))) -
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSub.hSub (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0))
          (∑ x : Fin (n + 1), (s.points j -ᵥ s.points 0))) +
    (s.points i -ᵥ s.points j) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
Tactic: simp_rw [h1 i, h1 j, sum_sub_distrib]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
          (HSub.hSub (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0))
            (∑ x : Fin (n + 1), (s.points i -ᵥ s.points 0))) -
        HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
          (HSub.hSub (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0))
            (∑ x : Fin (n + 1), (s.points j -ᵥ s.points 0))) +
      (s.points i -ᵥ s.points j) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ ((n + 1) • (s.points j -ᵥ s.points i)) + (s.points i -ᵥ s.points j) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
Tactic: rw [smul_sub, smul_sub, sub_sub_sub_cancel_left, ← smul_sub, ← sum_sub_distrib,
    vsub_sub_vsub_cancel_right, sum_const, card_univ, Fintype.card_fin]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ ((n + 1) • (s.points j -ᵥ s.points i)) + (s.points i -ᵥ s.points j) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
have this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
Tactic: have : (s.points i -ᵥ s.points j) = -(s.points j -ᵥ s.points i) := 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ ((n + 1) • (s.points j -ᵥ s.points i)) + (s.points i -ᵥ s.points j) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
Tactic: rw [this, ← sub_eq_add_neg, add_smul, sub_eq_iff_eq_add, one_smul, smul_add, add_comm]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.points j -ᵥ s.points i))
have norm_cast0 : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i))
Tactic: norm_cast0
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
this : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
have this₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.points j -ᵥ s.points i))
Tactic: have : (n : k)⁻¹ • n • (s.points j -ᵥ s.points i) =
      (n : k)⁻¹ • (n : k) • (s.points j -ᵥ s.points i) := by
    norm_cast0
    congr 1
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
this_1 : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
this :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.points j -ᵥ s.points i))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.points j -ᵥ s.points i)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
Tactic: rw [this, smul_smul, inv_eq_one_div, one_div_mul_cancel (NeZero.ne (n : k)), 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i j : Fin (n + 1)
h1 :
  ∀ (i : Fin (n + 1)),
    Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)))
this_1 : s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)
this :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.points j -ᵥ s.points i))
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (n • (s.points j -ᵥ s.points i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) +
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.points j -ᵥ s.points i) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
Tactic: rw [this, smul_smul, inv_eq_one_div, one_div_mul_cancel (NeZero.ne (n : k)), one_smul]