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 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)
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)
⊢ 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₂ : HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) +
    (HDiv.hDiv (α := k) 1 (↑n : k) * (↑n : k)) • (s.points j -ᵥ s.points i) =
  HDiv.hDiv (α := k) 1 (↑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)
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)
rw₂ :
  HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) +
      (HDiv.hDiv (α := k) 1 (↑n : k) * (↑n : k)) • (s.points j -ᵥ s.points i) =
    HDiv.hDiv (α := k) 1 (↑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₃ : HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) +
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.points j -ᵥ s.points i) =
  HDiv.hDiv (α := k) 1 (↑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)
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)
rw₂ :
  HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) +
      (HDiv.hDiv (α := k) 1 (↑n : k) * (↑n : k)) • (s.points j -ᵥ s.points i) =
    HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i)
rw₃ :
  HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (s.points j -ᵥ s.points i) =
    HDiv.hDiv (α := k) 1 (↑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₄ : HDiv.hDiv (α := k) 1 (↑n : k) • (s.points j -ᵥ s.points i) + (s.points j -ᵥ s.points i) =
  HDiv.hDiv (α := k) 1 (↑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 : Fin (n + 1)
⊢ s.faceOppositeCentroid i -ᵥ s.points i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
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 (β := V) (HAdd.hAdd (α := k) (↑n : k) 1 * ((↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹))
    (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
Tactic: rw [← vsub_sub_vsub_cancel_right _ (s.centroid) (s.points i),
    faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, centroid_vsub_eq,
    ← sub_smul, smul_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)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1 * ((↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have e_a : (↑n : k)⁻¹ = HAdd.hAdd (α := k) (↑n : k) 1 * ((↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹)
Tactic: congr
-- 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 ≠ 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n : k)⁻¹ = HAdd.hAdd (α := k) (↑n : k) 1 * ((↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹)
have e_a : (↑n : k)⁻¹ = HAdd.hAdd (α := k) 1 (↑n : k)⁻¹ - 1
Tactic: rw [mul_sub, add_mul, mul_inv_cancel₀ (NeZero.ne (n : k)), mul_inv_cancel₀ (by norm_cast),
    one_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)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
have rw : -(s.faceOppositeCentroid i -ᵥ s.points i) = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, 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.faceOppositeCentroid i -ᵥ s.points i) = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
have rw₁ : -(HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)) =
  HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, 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.faceOppositeCentroid i -ᵥ s.points i) = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₁ :
  -(HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
have rw₂ : -HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid) =
  HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, 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.faceOppositeCentroid i -ᵥ s.points i) = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₁ :
  -(HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₂ :
  -HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
have rw₃ : - -HAdd.hAdd (α := k) (↑n : k) 1 • -(s.faceOppositeCentroid i -ᵥ s.centroid) =
  HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, 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.faceOppositeCentroid i -ᵥ s.points i) = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₁ :
  -(HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₂ :
  -HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₃ :
  - -HAdd.hAdd (α := k) (↑n : k) 1 • -(s.faceOppositeCentroid i -ᵥ s.centroid) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
have rw₄ : - -HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i) =
  HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, 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.faceOppositeCentroid i -ᵥ s.points i) = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₁ :
  -(HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₂ :
  -HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₃ :
  - -HAdd.hAdd (α := k) (↑n : k) 1 • -(s.faceOppositeCentroid i -ᵥ s.centroid) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
rw₄ :
  - -HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i) =
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
have rw₅ : HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i) =
  HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.faceOppositeCentroid i)
Tactic: rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, 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.points i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i)
have symm : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) = s.points i -ᵥ s.centroid
Tactic: 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 : ℕ
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.centroid -ᵥ s.faceOppositeCentroid i) = s.points i -ᵥ s.centroid
have rw : HSMul.hSMul (β := V) ((↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ - (↑n : k)⁻¹))
    (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) =
  HSMul.hSMul (β := V) (-(HAdd.hAdd (α := k) (↑n : k) 1)⁻¹) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
Tactic: rw [← vsub_sub_vsub_cancel_right _ _ (s.points i),
    faceOppositeCentroid_vsub_point_eq_smul_sum_vsub,
    centroid_vsub_eq, ← neg_vsub_eq_vsub_rev,
    centroid_vsub_eq, ← sub_smul, smul_smul, ← neg_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)
⊢ HSMul.hSMul (β := V) ((↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ - (↑n : k)⁻¹))
      (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) =
    HSMul.hSMul (β := V) (-(HAdd.hAdd (α := k) (↑n : k) 1)⁻¹) (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have e_a : (↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ - (↑n : k)⁻¹) = -(HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: congr
-- 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)
⊢ (↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ - (↑n : k)⁻¹) = -(HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have e_a : (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
  HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: simp_rw [mul_sub, sub_eq_iff_eq_add, neg_add_eq_sub]
-- 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)
⊢ (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
    HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have e_a : HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
  (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: 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 : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
    (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have e_a : 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: rw [sub_eq_iff_eq_add, mul_inv_cancel₀ (NeZero.ne (n : k))]
-- 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)
⊢ 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have this : (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: have : (↑n + (1 : k))⁻¹ = 1 * (↑n + (1 : k))⁻¹ := 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 : Fin (n + 1)
this : (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
⊢ 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have e_a : 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: nth_rw 2 [this]
-- 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)
this : (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 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 (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)
this : (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
⊢ 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have e_a : 1 = HAdd.hAdd (α := k) (↑n : k) 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
Tactic: rw [← add_mul, mul_inv_cancel₀ (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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
this : (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
e_a : 1 = HAdd.hAdd (α := k) (↑n : k) 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
⊢ 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
have e_a₁ : Eq.{u_1 + 1} (α := k) 1 1
Tactic: rw [← add_mul, mul_inv_cancel₀ (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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.centroid -ᵥ s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
have rw : -(s.points 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)
⊢ 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]