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 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)
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))
⊢ 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:
norm_cast0
-- 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)
⊢ 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:
congr 1
-- 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)
⊢ 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
-- 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_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)
rw₄ 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)
⊢ 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, smul_smul, inv_eq_one_div, one_div_mul_cancel (NeZero.ne (n : k)), one_smul]

Premises used: smul_smul, inv_eq_one_div, Nat.cast, one_smul, one_div_mul_cancel, 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 :
  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))
⊢ s.faceOppositeCentroid i -ᵥ s.points i = HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)

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]

Premises used: Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, Affine.Simplex.points, sub_smul, smul_smul, vsub_sub_vsub_cancel_right, Affine.Simplex.centroid, Affine.Simplex.centroid_vsub_eq
-- 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)
e_a : (↑n : k)⁻¹ = HAdd.hAdd (α := k) (↑n : k) 1 * ((↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 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))

Tactic:
congr
-- 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)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0

Tactic:
norm_cast
-- 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)
e_a : (↑n : k)⁻¹ = HAdd.hAdd (α := k) 1 (↑n : k)⁻¹ - 1
⊢ (↑n : k)⁻¹ = HAdd.hAdd (α := k) (↑n : k) 1 * ((↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹)

Tactic:
rw [mul_sub, add_mul, mul_inv_cancel₀ (NeZero.ne (n : k)), mul_inv_cancel₀ (by norm_cast),
    one_mul]

Premises used: add_mul, mul_inv_cancel₀, mul_sub, Nat.cast, one_mul, 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)
⊢ (↑n : k)⁻¹ = HAdd.hAdd (α := k) 1 (↑n : k)⁻¹ - 1

Tactic:
grind
-- 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.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)
rw₅ 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)

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]

Premises used: neg_smul, neg_smul_neg, neg_neg, Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_vsub, 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)
symm : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) = s.points i -ᵥ s.centroid
⊢ s.points i -ᵥ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i)

Tactic:
symm
-- 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 (β := 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))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.centroid -ᵥ s.faceOppositeCentroid i) = s.points i -ᵥ s.centroid

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]

Premises used: Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, Affine.Simplex.points, neg_smul, sub_smul, smul_smul, vsub_sub_vsub_cancel_right, neg_vsub_eq_vsub_rev, Affine.Simplex.centroid_vsub_eq
-- 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)
e_a : (↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ - (↑n : k)⁻¹) = -(HAdd.hAdd (α := k) (↑n : k) 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))

Tactic:
congr
-- 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)
e_a :
  (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
    HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
⊢ (↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ - (↑n : k)⁻¹) = -(HAdd.hAdd (α := k) (↑n : k) 1)⁻¹

Tactic:
simp_rw [mul_sub, sub_eq_iff_eq_add, neg_add_eq_sub]

Premises used: mul_sub, neg_add_eq_sub, sub_eq_iff_eq_add
-- 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)
e_a :
  HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
    (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
⊢ (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
    HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹

Tactic:
symm
-- 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)
e_a : 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
⊢ HMul.hMul (α := k) (↑n : k) (↑n : k)⁻¹ - (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ =
    (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹

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

Premises used: mul_inv_cancel₀, Nat.cast, sub_eq_iff_eq_add, 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)
⊢ (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹

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)
⊢ (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹

Tactic:
have : (↑n + (1 : k))⁻¹ = 1 * (↑n + (1 : k))⁻¹ := 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 : Fin (n + 1)
this : (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ = 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹
e_a : 1 = (↑n : k) * (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)⁻¹

Tactic:
nth_rw 2 [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
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)⁻¹
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0

Tactic:
norm_cast
-- 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)
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)⁻¹
e_a₁ e_a₂ : Eq.{u_1 + 1} (α := k) 1 1
⊢ 1 = (↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ + 1 * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹

Tactic:
rw [← add_mul, mul_inv_cancel₀ (by norm_cast)]

Premises used: add_mul, mul_inv_cancel₀
-- 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.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)
rw₅ 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)

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]

Premises used: neg_smul, neg_smul_neg, neg_neg, neg_vsub_eq_vsub_rev, Affine.Simplex.point_vsub_centroid_eq_smul_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 : 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)
rw₃ rw₄ : s.faceOppositeCentroid i -ᵥ s.centroid = 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)

Tactic:
rw [centroid_vsub_point_eq_smul_vsub, smul_smul, inv_mul_cancel₀ (NeZero.ne (n : k)), one_smul]

Premises used: smul_smul, Nat.cast, one_smul, inv_mul_cancel₀, Affine.Simplex.centroid_vsub_point_eq_smul_vsub, 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.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)
rw₃ rw₄ : s.centroid -ᵥ s.faceOppositeCentroid i = 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)

Tactic:
rw [point_vsub_centroid_eq_smul_vsub, smul_smul, inv_mul_cancel₀ (NeZero.ne (n : k)), one_smul]

Premises used: smul_smul, Nat.cast, one_smul, Affine.Simplex.point_vsub_centroid_eq_smul_vsub, inv_mul_cancel₀, 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.centroid = (s.centroid -ᵥ s.points i) +ᵥ s.points i
rw₁ rw₂ : s.centroid = s.centroid
⊢ s.centroid = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.points i

Tactic:
rw [← centroid_vsub_point_eq_smul_vsub, vsub_vadd]

Premises used: vsub_vadd, Affine.Simplex.centroid_vsub_point_eq_smul_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 : 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)
rw₄ rw₅ : s.faceOppositeCentroid i -ᵥ s.centroid = 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

Tactic:
rw [centroid_vsub_point_eq_smul_vsub, eq_vadd_iff_vsub_eq, smul_smul,
    inv_mul_cancel₀ (NeZero.ne (n : k)), one_smul]

Premises used: smul_smul, Nat.cast, one_smul, inv_mul_cancel₀, eq_vadd_iff_vsub_eq, Affine.Simplex.centroid_vsub_point_eq_smul_vsub, 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
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)
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₂)
⊢ (s.map f hf).faceOppositeCentroid i = (f : (a : P) → P₂) (s.faceOppositeCentroid i)

Tactic:
simp only [faceOppositeCentroid, faceOpposite_map, centroid_eq_affineCombination, map_points]

Premises used: Affine.Simplex.faceOpposite_map, Affine.Simplex.faceOppositeCentroid, Affine.Simplex.centroid_eq_affineCombination, Affine.Simplex.map_points