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 :
  -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₁ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid -ᵥ s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
have rw₂ : -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (-(s.centroid -ᵥ s.faceOppositeCentroid i)) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [← neg_vsub_eq_vsub_rev, point_vsub_centroid_eq_smul_vsub, ← neg_smul_neg,
    neg_vsub_eq_vsub_rev, ← neg_smul, neg_neg]
-- 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.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₁ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₂ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (-(s.centroid -ᵥ s.faceOppositeCentroid i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid -ᵥ s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
have rw₃ : -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [← neg_vsub_eq_vsub_rev, point_vsub_centroid_eq_smul_vsub, ← neg_smul_neg,
    neg_vsub_eq_vsub_rev, ← neg_smul, neg_neg]
-- 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.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₁ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₂ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (-(s.centroid -ᵥ s.faceOppositeCentroid i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid -ᵥ s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
have rw₄ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (- -(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [← neg_vsub_eq_vsub_rev, point_vsub_centroid_eq_smul_vsub, ← neg_smul_neg,
    neg_vsub_eq_vsub_rev, ← neg_smul, neg_neg]
-- 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.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₁ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₂ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (-(s.centroid -ᵥ s.faceOppositeCentroid i)) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (- -(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid -ᵥ s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
have rw₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [← neg_vsub_eq_vsub_rev, point_vsub_centroid_eq_smul_vsub, ← neg_smul_neg,
    neg_vsub_eq_vsub_rev, ← neg_smul, neg_neg]
-- 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 -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i)
have rw : s.faceOppositeCentroid i -ᵥ s.centroid =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
Tactic: rw [centroid_vsub_point_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i)
have rw₁ : s.faceOppositeCentroid i -ᵥ s.centroid =
  HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [centroid_vsub_point_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
rw₁ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i)
have rw₂ : s.faceOppositeCentroid i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [centroid_vsub_point_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
rw₁ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₂ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.faceOppositeCentroid i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i)
have rw₃ : s.faceOppositeCentroid i -ᵥ s.centroid = s.faceOppositeCentroid i -ᵥ s.centroid
Tactic: rw [centroid_vsub_point_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i -ᵥ s.centroid)
have rw : s.centroid -ᵥ s.faceOppositeCentroid i =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i))
Tactic: rw [point_vsub_centroid_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
rw :
  s.centroid -ᵥ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i))
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i -ᵥ s.centroid)
have rw₁ : s.centroid -ᵥ s.faceOppositeCentroid i =
  HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [point_vsub_centroid_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
rw :
  s.centroid -ᵥ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i))
rw₁ :
  s.centroid -ᵥ s.faceOppositeCentroid i =
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i -ᵥ s.centroid)
have rw₂ : s.centroid -ᵥ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [point_vsub_centroid_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
rw :
  s.centroid -ᵥ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i))
rw₁ :
  s.centroid -ᵥ s.faceOppositeCentroid i =
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₂ :
  s.centroid -ᵥ s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points i -ᵥ s.centroid)
have rw₃ : s.centroid -ᵥ s.faceOppositeCentroid i = s.centroid -ᵥ s.faceOppositeCentroid i
Tactic: rw [point_vsub_centroid_eq_smul_vsub, smul_smul, inv_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 : Fin (n + 1)
⊢ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.points i
have rw : s.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i
Tactic: rw [← centroid_vsub_point_eq_smul_vsub, 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.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i
⊢ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.points i
have rw₁ : s.centroid = s.centroid
Tactic: rw [← centroid_vsub_point_eq_smul_vsub, 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.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid
have rw : s.faceOppositeCentroid i =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)) +ᵥ
    s.centroid
Tactic: rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)) +ᵥ
      s.centroid
⊢ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid
have rw₁ : s.faceOppositeCentroid i -ᵥ s.centroid =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
Tactic: rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)) +ᵥ
      s.centroid
rw₁ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
⊢ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid
have rw₂ : s.faceOppositeCentroid i -ᵥ s.centroid =
  HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)) +ᵥ
      s.centroid
rw₁ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
rw₂ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid
have rw₃ : s.faceOppositeCentroid i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_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 : Fin (n + 1)
rw :
  s.faceOppositeCentroid i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
        (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)) +ᵥ
      s.centroid
rw₁ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹
      (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid))
rw₂ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HMul.hMul (α := k) (↑n : k)⁻¹ (↑n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  s.faceOppositeCentroid i -ᵥ s.centroid =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.faceOppositeCentroid i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid
have rw₄ : s.faceOppositeCentroid i -ᵥ s.centroid = s.faceOppositeCentroid i -ᵥ s.centroid
Tactic: rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_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
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : Fin (n + 1)
⊢ (s.map f hf).faceOppositeCentroid i = (f : (a : P) → P₂) (s.faceOppositeCentroid i)
have simp : Eq.{u_5 + 1} (α := P₂)
  ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ (s.faceOpposite i).points) : (a : Fin (n - 1 + 1) → k) → P₂)
      (centroidWeights k univ) :
    P₂)
  ((f : (a : P) → P₂)
      ((affineCombination k univ (s.faceOpposite i).points : (a : Fin (n - 1 + 1) → k) → P) (centroidWeights k univ) :
        P) :
    P₂)
Tactic: simp only [faceOppositeCentroid, faceOpposite_map, centroid_eq_affineCombination, map_points]
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : Fin (n + 1)
⊢ Eq.{u_5 + 1} (α := P₂)
    ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ (s.faceOpposite i).points) : (a : Fin (n - 1 + 1) → k) → P₂)
        (centroidWeights k univ) :
      P₂)
    ((f : (a : P) → P₂)
        ((affineCombination k univ (s.faceOpposite i).points : (a : Fin (n - 1 + 1) → k) → P) (centroidWeights k univ) :
          P) :
      P₂)
have hw : Finset.sum (ι := Fin (n - 1 + 1)) univ (centroidWeights k univ) = 1
Tactic: rw [Finset.map_affineCombination]
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : Fin (n + 1)
⊢ Finset.sum (ι := Fin (n - 1 + 1)) univ (centroidWeights k univ) = 1
have hw : card (α := Fin (n - 1 + 1)) univ ≠ 0
Tactic: rw [sum_centroidWeights_eq_one_of_card_ne_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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (↑((s.restrict S hS).faceOppositeCentroid i) : P) = s.faceOppositeCentroid i
have rw : s.faceOppositeCentroid i = (↑((s.restrict S hS).faceOppositeCentroid i) : P)
Tactic: rw [eq_comm]
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i = (↑((s.restrict S hS).faceOppositeCentroid i) : P)
have this : Nonempty.{u_3 + 1} ↥S
Tactic: haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_3 + 1} ↥S
⊢ s.faceOppositeCentroid i = (↑((s.restrict S hS).faceOppositeCentroid i) : P)
have hf : Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)
Tactic: have hf : Function.Injective (S.subtype) := by
    simp only [coe_subtype, Subtype.val_injective]
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).faceOppositeCentroid = s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))
have h : ∀ (i : Fin (n + 1)),
  (s.reindex e).faceOppositeCentroid i = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i
Tactic: ext i