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

Tactic:
norm_cast 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
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)
i : Fin (n + 1)
ha :
  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)
⊢ ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0

Tactic:
have key : ∀ n : ℕ, (n : k) + 1 ≠ 0 := fun n h => by norm_cast 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
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)
i : Fin (n + 1)
ha :
  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)
key : ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
h₃ : i ∈ fs₁ → i ∈ fs₂
h₄ : i ∈ fs₂ → i ∈ fs₁
⊢ i ∈ fs₁ ↔ i ∈ fs₂

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
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)
i : Fin (n + 1)
ha :
  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)
key : ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
hi : i ∈ fs₁
h₃ : ∀ (hni : i ∉ fs₂), False
⊢ i ∈ fs₂

Tactic:
by_contra hni
-- 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)
i : Fin (n + 1)
ha :
  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)
key : ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
hi : i ∈ fs₂
h₃ : ∀ (hni : i ∉ fs₁), False
⊢ i ∈ fs₁

Tactic:
by_contra hni
-- 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)
i : Fin (n + 1)
ha :
  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)
key : ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
hi : i ∈ fs₁
hni : i ∉ fs₂
⊢ False

Tactic:
simp [hni, hi, key] at ha
-- 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)
i : Fin (n + 1)
ha :
  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)
key : ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
hi : i ∈ fs₂
hni : i ∉ fs₁
⊢ False

Tactic:
simpa [hni, hi, key] using ha.symm

Premises used: 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
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
rw : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂
⊢ Finset.centroid k univ (s.face h₁).points = Finset.centroid k univ (s.face h₂).points ↔ fs₁ = fs₂

Tactic:
rw [face_centroid_eq_centroid, face_centroid_eq_centroid]

Premises used: Affine.Simplex.face_centroid_eq_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
⊢ Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂

Tactic:
s.centroid_eq_iff h₁ h₂

Premises used: Affine.Simplex.centroid_eq_iff
-- 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:
exact s.centroid_eq_iff h₁ h₂

Premises used: Affine.Simplex.centroid_eq_iff
-- 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₁ s₂ : Simplex k P n
h : Set.range s₁.points = Set.range s₂.points
⊢ s₁.points '' (↑univ : Set (Fin (n + 1))) = s₂.points '' (↑univ : Set (Fin (n + 1)))

Tactic:
rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h

Premises used: Set.image_univ, Finset.coe_univ
-- 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₁ s₂ : Simplex k P n
h : s₁.points '' (↑univ : Set (Fin (n + 1))) = s₂.points '' (↑univ : Set (Fin (n + 1)))
⊢ Finset.centroid k univ s₁.points = Finset.centroid k univ s₂.points

Tactic:
Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
      (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
      (fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h

Premises used: Finset.univ, AffineIndependent.injective, Affine.Simplex.independent, Finset.centroid_eq_of_inj_on_of_image_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 : ℕ
s₁ s₂ : Simplex k P n
h : s₁.points '' (↑univ : Set (Fin (n + 1))) = s₂.points '' (↑univ : Set (Fin (n + 1)))
⊢ Finset.centroid k univ s₁.points = Finset.centroid k univ s₂.points

Tactic:
exact
    Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
      (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
      (fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h

Premises used: Finset.univ, AffineIndependent.injective, Affine.Simplex.independent, Finset.centroid_eq_of_inj_on_of_image_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)
⊢ Ne (α := Set (Fin (n + 1))) {i}ᶜ Set.univ

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 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.centroid ∉ affineSpan k (s.points '' {i}ᶜ)

Tactic:
have : s.centroid ∉ affineSpan k (s.points '' {i}ᶜ) :=
    s.centroid_notMem_affineSpan_of_ne_univ (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 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
this : s.centroid ∉ affineSpan k (s.points '' {i}ᶜ)
⊢ AffineIndependent k (Function.update (β := fun (a : Fin (n + 1)) ↦ P) s.points i s.centroid)

Tactic:
AffineIndependent.affineIndependent_update_of_notMem_affineSpan s.independent this

Premises used: Affine.Simplex.independent, AffineIndependent.affineIndependent_update_of_notMem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
this : s.centroid ∉ affineSpan k (s.points '' {i}ᶜ)
⊢ AffineIndependent k (Function.update (β := fun (a : Fin (n + 1)) ↦ P) s.points i s.centroid)

Tactic:
exact AffineIndependent.affineIndependent_update_of_notMem_affineSpan s.independent this

Premises used: Affine.Simplex.independent, AffineIndependent.affineIndependent_update_of_notMem_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
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 : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
rw :
  Eq.{u_5 + 1} (α := P₂) (Finset.centroid k univ ((⇑f : (a : P) → P₂) ∘ s.points) : P₂)
    ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ s.points) : (a : Fin (n + 1) → k) → P₂) (centroidWeights k univ) :
      P₂)
hw : Finset.sum (ι := Fin (n + 1)) univ (centroidWeights k univ) = 1
⊢ (s.map f hf).centroid = (f : (a : P) → P₂) s.centroid

Tactic:
rw [centroid, map_points, centroid_eq_affineCombination, Finset.map_affineCombination]

Premises used: Finset.map_affineCombination, Affine.Simplex.centroid_eq_affineCombination, Affine.Simplex.centroid, Affine.Simplex.map_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
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
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₂)
rw rw₁ :
  Eq.{u_5 + 1} (α := P₂)
    ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ s.points) : (a : Fin (n + 1) → k) → P₂) (centroidWeights k univ) :
      P₂)
    ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ s.points) : (a : Fin (n + 1) → k) → P₂) (centroidWeights k univ) :
      P₂)
⊢ Eq.{u_5 + 1} (α := P₂) (Finset.centroid k univ ((⇑f : (a : P) → P₂) ∘ s.points) : P₂)
    ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ s.points) : (a : Fin (n + 1) → k) → P₂) (centroidWeights k univ) :
      P₂)

Tactic:
rw [Finset.centroid]

Premises used: 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
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
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₂)
hw : card (α := Fin (n + 1)) univ ≠ 0
⊢ Finset.sum (ι := Fin (n + 1)) univ (centroidWeights k univ) = 1

Tactic:
rw [sum_centroidWeights_eq_one_of_card_ne_zero]

Premises used: Finset.sum_centroidWeights_eq_one_of_card_ne_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
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 : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ card (α := Fin (n + 1)) univ ≠ 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
simp :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (s.reindex e).points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P)
    ((affineCombination k univ s.points : (a : Fin (m + 1) → k) → P) (centroidWeights k univ) : P)
⊢ Finset.centroid k univ (s.reindex e).points = Finset.centroid k univ s.points

Tactic:
simp only [centroid_eq_affineCombination]

Premises used: Affine.Simplex.centroid_eq_affineCombination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
simp :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) : (a : Fin (n + 1) → k) → P)
        (centroidWeights k univ) :
      P)
    ((affineCombination k univ s.points : (a : Fin (m + 1) → k) → P) (centroidWeights k univ) : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (s.reindex e).points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P)
    ((affineCombination k univ s.points : (a : Fin (m + 1) → k) → P) (centroidWeights k univ) : P)

Tactic:
simp only [reindex]

Premises used: Affine.Simplex.reindex
-- 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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ m = n

Tactic:
simpa using Fintype.card_eq.2 ⟨e⟩

Premises used: Iff.mpr, Fintype.card_eq, Nonempty.intro
-- 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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ m = n

Tactic:
have h_eq : m = n := by simpa using Fintype.card_eq.2 ⟨e⟩
-- 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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
h_eq : m = n
subst :
  ∀ (e : Fin (m + 1) ≃ Fin (m + 1)),
    Eq.{u_3 + 1} (α := P)
      ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1))) : (a : Fin (m + 1) → k) → P)
          (centroidWeights k univ) :
        P)
      ((affineCombination k univ s.points : (a : Fin (m + 1) → k) → P) (centroidWeights k univ) : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) : (a : Fin (n + 1) → k) → P)
        (centroidWeights k univ) :
      P)
    ((affineCombination k univ s.points : (a : Fin (m + 1) → k) → P) (centroidWeights k univ) : P)

Tactic:
subst h_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
m : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (m + 1)
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k (Finset.map e.toEmbedding univ) (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1))) :
          (a : Fin (m + 1) → k) → P)
        (centroidWeights k univ) :
      P)
    ((affineCombination k univ
            (Function.comp (β := Fin (m + 1)) (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1)))
              (⇑e.toEmbedding : (a : Fin (m + 1)) → Fin (m + 1))) :
          (a : Fin (m + 1) → k) → P)
        (Function.comp (β := Fin (m + 1)) (centroidWeights k univ) (⇑e.toEmbedding : (a : Fin (m + 1)) → Fin (m + 1))) :
      P)

Tactic:
Finset.univ.affineCombination_map e.toEmbedding _ _

Premises used: Finset.univ, Finset.affineCombination_map, Equiv.toEmbedding
-- 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
m : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (m + 1)
h : univ = Finset.map e.toEmbedding univ
h₁ :
  s.points =
    Function.comp (β := Fin (m + 1)) (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1)))
      (⇑e.toEmbedding : (a : Fin (m + 1)) → Fin (m + 1))
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1))) : (a : Fin (m + 1) → k) → P)
        (centroidWeights k univ) :
      P)
    ((affineCombination k univ s.points : (a : Fin (m + 1) → k) → P) (centroidWeights k univ) : P)

Tactic:
convert! Finset.univ.affineCombination_map e.toEmbedding _ _

Premises used: Finset.univ, Finset.affineCombination_map, Equiv.toEmbedding
-- 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
m : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (m + 1)
⊢ univ = Finset.map e.toEmbedding univ

Tactic:
simp [Function.comp_assoc]

Premises used: Function.comp_assoc
-- 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
m : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (m + 1)
⊢ s.points =
    Function.comp (β := Fin (m + 1)) (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1)))
      (⇑e.toEmbedding : (a : Fin (m + 1)) → Fin (m + 1))

Tactic:
simp [Function.comp_assoc]

Premises used: Function.comp_assoc
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
rw : s.centroid = (↑(s.restrict S hS).centroid : P)
⊢ (↑(s.restrict S hS).centroid : P) = s.centroid

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ Nonempty.{u_3 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)

Tactic:
simp only [coe_subtype, Subtype.val_injective]

Premises used: Subtype.val_injective, AffineSubspace.coe_subtype
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
⊢ 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]
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
hf : Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)
⊢ s.centroid = (↑(s.restrict S hS).centroid : P)

Tactic:
(s.restrict S hS).centroid_map S.subtype hf

Premises used: Affine.Simplex.centroid_map, AffineSubspace.subtype, Affine.Simplex.restrict
-- 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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
hf : Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)
⊢ s.centroid = (↑(s.restrict S hS).centroid : P)

Tactic:
exact (s.restrict S hS).centroid_map S.subtype hf

Premises used: Affine.Simplex.centroid_map, AffineSubspace.subtype, Affine.Simplex.restrict