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 : CharZero k
s : Simplex k P n
p : P
rw :
  ∑ i : Fin (n + 1), centroidWeights k univ i • (s.points i -ᵥ p) =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ p))
⊢ s.centroid -ᵥ p = HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ p))

Tactic:
rw [centroid_vsub_const _ _ (by simp), centroid_def, affineCombination_eq_linear_combination
    (hw := sum_centroidWeights_eq_one_of_nonempty _ _ (by simp))]

Premises used: Finset.affineCombination_eq_linear_combination, Finset.centroid_vsub_const, Finset.sum_centroidWeights_eq_one_of_nonempty, Finset.centroidWeights, 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 : CharZero k
s : Simplex k P n
p : P
⊢ ∑ i : Fin (n + 1), centroidWeights k univ i • (s.points i -ᵥ p) =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ p))

Tactic:
simp [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 : 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 (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)) +ᵥ s.points i

Tactic:
rw [← s.centroid_vsub_eq, vsub_vadd]

Premises used: vsub_vadd, 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 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
rw : HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
⊢ HAdd.hAdd (α := k) (↑n : k) 1 • (s.centroid -ᵥ s.points i) = ∑ x : Fin (n + 1), (s.points x -ᵥ s.points i)

Tactic:
rw [centroid_eq_smul_sum_vsub_vadd s i, vadd_vsub, smul_smul, mul_inv_cancel₀, one_smul]

Premises used: Affine.Simplex.centroid_eq_smul_sum_vsub_vadd, mul_inv_cancel₀, smul_smul, one_smul, 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 : 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 : CharZero k
s : Simplex k P n
⊢ s.centroid -ᵥ s.centroid =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))

Tactic:
have h := centroid_vsub_eq s s.centroid
-- 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 : CharZero k
s : Simplex k P n
h :
  s.centroid -ᵥ s.centroid =
    HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))
⊢ 0 = HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))

Tactic:
simp only [vsub_self] at h

Premises used: vsub_self
-- 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 : CharZero k
s : Simplex k P n
h : 0 = HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid))
⊢ HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) = 0

Tactic:
symm at h
-- 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 : CharZero k
s : Simplex k P n
h : HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) = 0
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 : CharZero k
s : Simplex k P n
h : HSMul.hSMul (β := V) (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) 0

Tactic:
rw [smul_eq_zero_iff_right (inv_ne_zero (by norm_cast))] at h

Premises used: smul_eq_zero_iff_right
-- 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 : CharZero k
s : Simplex k P n
h : Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0

Tactic:
h
-- 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 : CharZero k
s : Simplex k P n
h : Eq.{u_2 + 1} (α := V) (∑ x : Fin (n + 1), (s.points x -ᵥ s.centroid)) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0

Tactic:
exact h
-- 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 : CharZero k
s : Simplex k P n
p : P
mp : p = s.centroid → Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
mpr : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0 → p = s.centroid
⊢ p = s.centroid ↔ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0

Tactic:
constructor
-- 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 : CharZero k
s : Simplex k P n
p : P
h : p = s.centroid
mp : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid)) 0
mp₁ mp₂ : Eq.{u_2 + 1} (α := V) 0 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0

Tactic:
rw [h, centroid_weighted_vsub_eq_zero]

Premises used: Affine.Simplex.centroid_weighted_vsub_eq_zero
-- 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 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
mpr : p -ᵥ s.centroid = 0
⊢ p = s.centroid

Tactic:
rw [← vsub_eq_zero_iff_eq]

Premises used: vsub_eq_zero_iff_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 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
apply :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) univ x → s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))

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 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
x : Fin (n + 1)
hx : Membership.mem (γ := Finset (Fin (n + 1))) univ x
rw rw₁ : s.points x -ᵥ p = s.points x -ᵥ p
⊢ s.points x -ᵥ p = s.points x -ᵥ s.centroid - (p -ᵥ s.centroid)

Tactic:
rw [vsub_sub_vsub_cancel_right _ _ s.centroid]

Premises used: vsub_sub_vsub_cancel_right, Affine.Simplex.centroid
-- 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 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))

Tactic:
have : ∑ i, (s.points i -ᵥ p) = ∑ i, ((s.points i -ᵥ s.centroid) - (p -ᵥ s.centroid)) := by
      apply sum_congr rfl
      intro x hx
      rw [vsub_sub_vsub_cancel_right _ _ s.centroid]
-- 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 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
⊢ HSub.hSub (α := V) 0 (∑ x : Fin (n + 1), (p -ᵥ s.centroid)) = 0

Tactic:
rw [this, sum_sub_distrib, centroid_weighted_vsub_eq_zero] at h

Premises used: Affine.Simplex.centroid_weighted_vsub_eq_zero, 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 : CharZero k
s : Simplex k P n
p : P
h : Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p)) 0
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h₁ : HSub.hSub (α := V) 0 (∑ x : Fin (n + 1), (p -ᵥ s.centroid)) = 0
⊢ Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))

Tactic:
rw [this, sum_sub_distrib, centroid_weighted_vsub_eq_zero] at h

Premises used: Affine.Simplex.centroid_weighted_vsub_eq_zero, 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 : CharZero k
s : Simplex k P n
p : P
h : HSub.hSub (α := V) 0 (∑ x : Fin (n + 1), (p -ᵥ s.centroid)) = 0
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
⊢ (n + 1) • (p -ᵥ s.centroid) = 0

Tactic:
simp only [sum_const, card_univ, Fintype.card_fin, zero_sub, neg_eq_zero] at h

Premises used: Finset.card_univ, Fintype.card_fin, neg_eq_zero, zero_sub, 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 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (n + 1) • (p -ᵥ s.centroid) = 0
⊢ HAdd.hAdd (α := k) (↑n : k) 1 • (p -ᵥ s.centroid) = 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 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
⊢ HAdd.hAdd (α := k) (↑n : k) 1 • (p -ᵥ s.centroid) = 0

Tactic:
have h' : ((n : k) + 1) • (p -ᵥ s.centroid) = 0 := by 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 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : HAdd.hAdd (α := k) (↑n : k) 1 • (p -ᵥ s.centroid) = 0
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 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : HAdd.hAdd (α := k) (↑n : k) 1 • (p -ᵥ s.centroid) = 0
⊢ p -ᵥ s.centroid = 0

Tactic:
rw [smul_eq_zero_iff_right (by norm_cast)] at h'

Premises used: smul_eq_zero_iff_right
-- 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 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : p -ᵥ s.centroid = 0
⊢ p -ᵥ s.centroid = 0

Tactic:
h'
-- 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 : CharZero k
s : Simplex k P n
p : P
this :
  Eq.{u_2 + 1} (α := V) (∑ i : Fin (n + 1), (s.points i -ᵥ p))
    (∑ i : Fin (n + 1), (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid)))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : p -ᵥ s.centroid = 0
⊢ p -ᵥ s.centroid = 0

Tactic:
exact h'
-- 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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ Finset.centroid k (ι := Fin (m + 1)) univ
      (s.points ∘
        (⇑(RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦
              x1 ≤ x2) (fs.orderEmbOfFin h)) :
          (a : Fin (m + 1)) → Fin (n + 1))) =
    Finset.centroid k
      (Finset.map
        (RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
          (fs.orderEmbOfFin h))
        univ)
      s.points

Tactic:
(Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm

Premises used: Affine.Simplex.points, Finset.orderEmbOfFin, Finset.univ, Finset.centroid_map, RelEmbedding.toEmbedding, Eq.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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
h₁ :
  fs =
    Finset.map
      (RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
        (fs.orderEmbOfFin h))
      univ
⊢ Finset.centroid k univ (s.face h).points = Finset.centroid k fs s.points

Tactic:
convert! (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm

Premises used: Affine.Simplex.points, Finset.orderEmbOfFin, Finset.univ, Finset.centroid_map, RelEmbedding.toEmbedding, Eq.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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
h₁ :
  (↑fs : Set (Fin (n + 1))) =
    Set.range (ι := Fin (m + 1))
      (⇑(RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
            (fs.orderEmbOfFin h)) :
        (a : Fin (m + 1)) → Fin (n + 1))
⊢ fs =
    Finset.map
      (RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
        (fs.orderEmbOfFin h))
      univ

Tactic:
rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_inj, Finset.coe_map
-- 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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ (↑fs : Set (Fin (n + 1))) =
    Set.range (ι := Fin (m + 1))
      (⇑(RelEmbedding.toEmbedding (r := fun (x1 x2 : Fin (m + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2)
            (fs.orderEmbOfFin h)) :
        (a : Fin (m + 1)) → Fin (n + 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
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
⊢ Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂

Tactic:
⟨fun h => ?_, @congrArg _ _ fs₁ fs₂ (fun z => Finset.centroid k z s.points)⟩

Premises used: Affine.Simplex.points, congrArg, Iff.intro, Finset.centroid
-- 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
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
refine : ∀ (h : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points), fs₁ = fs₂
⊢ Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂

Tactic:
refine ⟨fun h => ?_, @congrArg _ _ fs₁ fs₂ (fun z => Finset.centroid k z s.points)⟩
-- 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
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)

Tactic:
rw [Finset.centroid_eq_affineCombination_fintype,
    Finset.centroid_eq_affineCombination_fintype] at h

Premises used: Finset.centroid_eq_affineCombination_fintype
-- 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
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
⊢ (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₁) =
    (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₂)

Tactic:
have ha :=
    (affineIndependent_iff_indicator_eq_of_affineCombination_eq k s.points).1 s.independent _ _ _ _
      (fs₁.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₁)
      (fs₂.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₂) h
-- 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
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
ha :
  (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₁) =
    (↑univ : Set (Fin (n + 1))).indicator (centroidWeightsIndicator k fs₂)
⊢ ∀ (x : Fin (n + 1)),
    Eq.{u_1 + 1} (α := k) ((↑fs₁ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1) : k)⁻¹) x)
      ((↑fs₂ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1) : k)⁻¹) x)

Tactic:
simp_rw [Finset.coe_univ, Set.indicator_univ, funext_iff,
    Finset.centroidWeightsIndicator_def, Finset.centroidWeights, h₁, h₂] at ha

Premises used: Finset.coe_univ, funext_iff, Finset.centroidWeightsIndicator_def, Set.indicator_univ, Finset.centroidWeights
-- 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
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
ha :
  ∀ (x : Fin (n + 1)),
    Eq.{u_1 + 1} (α := k) ((↑fs₁ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1) : k)⁻¹) x)
      ((↑fs₂ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1) : k)⁻¹) x)
h₃ : ∀ (i : Fin (n + 1)), i ∈ fs₁ ↔ i ∈ fs₂
⊢ fs₁ = fs₂

Tactic:
ext i
-- 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
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₁) : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeightsIndicator k fs₂) : P)
ha :
  ∀ (x : Fin (n + 1)),
    Eq.{u_1 + 1} (α := k) ((↑fs₁ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1) : k)⁻¹) x)
      ((↑fs₂ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1) : k)⁻¹) x)
i : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := k) ((↑fs₁ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₁ + 1) : k)⁻¹) i)
    ((↑fs₂ : Set (Fin (n + 1))).indicator (Function.const (Fin (n + 1)) (↑(m₂ + 1) : k)⁻¹) i)

Tactic:
specialize ha i