awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
    (s.faceOppositeCentroid i)

Tactic:
centroid_mem_affineSpan (s.faceOpposite i)

Premises used: Affine.Simplex.faceOppositeCentroid, Set.Mem, Finset.centroid, Affine.Simplex.faceOpposite, Affine.Simplex.centroid_mem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
unfold :
  (s.faceOpposite i).centroid =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
⊢ s.faceOppositeCentroid i =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹

Tactic:
unfold faceOppositeCentroid

Premises used: Affine.Simplex.faceOppositeCentroid
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1

Tactic:
simp [card_compl, NeZero.one_le]

Premises used: Finset.card_compl, NeZero.one_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯

Tactic:
have : s.faceOpposite i = s.face (fs := {i}ᶜ) (by simp [card_compl, NeZero.one_le]) := by rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
rw :
  (s.face (fs := {i}ᶜ) ⋯).centroid =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
⊢ (s.faceOpposite i).centroid =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P)
        (Function.const (Fin (n + 1)) (↑(Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i}) : k)⁻¹) :
      P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)
⊢ Finset.centroid k univ (s.face (fs := {i}ᶜ) ⋯).points =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹

Tactic:
rw [face_centroid_eq_centroid, centroid_def, centroidWeights_eq_const, card_compl]

Premises used: Finset.card_compl, Affine.Simplex.face_centroid_eq_centroid, Finset.centroidWeights_eq_const, Finset.centroid_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
simp :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) (Function.const (Fin (n + 1)) (↑n : k)⁻¹) : P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P)
        (Function.const (Fin (n + 1)) (↑(Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i}) : k)⁻¹) :
      P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)

Tactic:
simp only [Fintype.card_fin, card_singleton, add_tsub_cancel_right]

Premises used: Fintype.card_fin, add_tsub_cancel_right, Finset.card_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) (Function.const (Fin (n + 1)) (↑n : k)⁻¹) : P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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))
rw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ {i}ᶜ, (↑n : k)⁻¹) 1
⊢ 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))

Tactic:
rw [faceOppositeCentroid_eq_affineCombination,
    affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ ?_ (s.points i)]

Premises used: Affine.Simplex.points, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Affine.Simplex.faceOppositeCentroid_eq_affineCombination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
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))
⊢ 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))

Tactic:
simp only [weightedVSubOfPoint_apply, vadd_vsub]

Premises used: Finset.weightedVSubOfPoint_apply, vadd_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
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))
⊢ 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:
rw [← Finset.sum_compl_add_sum {i}]

Premises used: Finset.sum_compl_add_sum, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
⊢ ∑ 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:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 : 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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))
rw₁ 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))
⊢ ∑ 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:
rw [h i, smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
simp : HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ = 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ {i}ᶜ, (↑n : k)⁻¹) 1

Tactic:
simp only [sum_const, card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right,
      nsmul_eq_mul]

Premises used: Fintype.card_fin, Finset.card_compl, nsmul_eq_mul, add_tsub_cancel_right, Finset.sum_const, Finset.card_singleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 rw₁ : Eq.{u_1 + 1} (α := k) 1 1
⊢ HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ = 1

Tactic:
rw [mul_inv_cancel₀ (NeZero.ne (n : k))]

Premises used: mul_inv_cancel₀, Nat.cast, NeZero.ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
rw₁ rw₂ : s.faceOppositeCentroid i = s.faceOppositeCentroid 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

Tactic:
rw [← faceOppositeCentroid_vsub_point_eq_smul_sum_vsub s i, vsub_vadd]

Premises used: Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, vsub_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 :
  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))
⊢ 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))

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]

Premises used: Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, neg_smul, smul_smul, neg_vsub_eq_vsub_rev, Finset.smul_sum, Lean.Grind.Ring.neg_eq_mul_neg_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
⊢ 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:
simp only [neg_smul, one_smul, neg_vsub_eq_vsub_rev]

Premises used: neg_smul, one_smul, neg_vsub_eq_vsub_rev
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.points i) =
    ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)

Tactic:
simp [faceOppositeCentroid_eq_sum_vsub_vadd, smul_smul, mul_inv_cancel₀ (NeZero.ne (n : k)),
    one_smul]

Premises used: mul_inv_cancel₀, smul_smul, Nat.cast, one_smul, Affine.Simplex.faceOppositeCentroid_eq_sum_vsub_vadd, NeZero.ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
rw₁ 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))
⊢ 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)

Tactic:
rw [smul_faceOppositeCentroid_vsub_point_eq_sum_vsub s i,
    smul_centroid_vsub_point_eq_sum_vsub s i]

Premises used: Affine.Simplex.smul_faceOppositeCentroid_vsub_point_eq_sum_vsub, Affine.Simplex.smul_centroid_vsub_point_eq_sum_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
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)
⊢ s.faceOppositeCentroid i -ᵥ s.faceOppositeCentroid 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)]

Premises used: Affine.Simplex.points, Affine.Simplex.faceOppositeCentroid_eq_sum_vsub_vadd, vadd_vsub_vadd_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
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)
⊢ 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:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
⊢ ∀ (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:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
⊢ ∀ (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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)))
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)
⊢ 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:
simp_rw [h1 i, h1 j, sum_sub_distrib]

Premises used: Finset.sum_sub_distrib
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)))
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)
⊢ 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:
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]

Premises used: Finset.card_univ, Fintype.card_fin, smul_sub, Finset.sum_sub_distrib, vsub_sub_vsub_cancel_right, sub_sub_sub_cancel_left, Finset.sum_const
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)))
⊢ s.points i -ᵥ s.points j = -(s.points j -ᵥ s.points i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)))
⊢ 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
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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)
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)
⊢ 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 [this, ← sub_eq_add_neg, add_smul, sub_eq_iff_eq_add, one_smul, smul_add, add_comm]

Premises used: sub_eq_add_neg, add_comm, one_smul, add_smul, sub_eq_iff_eq_add, smul_add