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
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)
⊢ fs₁ = fs₂
have h₃ : ∀ (i : Fin (n + 1)), i ∈ fs₁ ↔ i ∈ fs₂
Tactic: ext i
-- 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
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)
⊢ i ∈ fs₁ ↔ i ∈ fs₂
have 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)
Tactic: specialize ha i
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
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
⊢ False
have norm_cast : ∀ (h : False), False
Tactic: norm_cast at h
Cleared hypotheses: h
-- 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
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)
⊢ i ∈ fs₁ ↔ i ∈ fs₂
have key : ∀ (n : ℕ), HAdd.hAdd (α := k) (↑n : k) 1 ≠ 0
Tactic: have key : ∀ n : ℕ, (n : k) + 1 ≠ 0 := fun n h => by norm_cast at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
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
⊢ i ∈ fs₁ ↔ i ∈ fs₂
have h₃ : i ∈ fs₁ → i ∈ fs₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
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₂
⊢ i ∈ fs₁ ↔ i ∈ fs₂
have h₄ : i ∈ fs₂ → i ∈ fs₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
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₁
⊢ i ∈ fs₂
have h₃ : ∀ (hni : i ∉ fs₂), False
Tactic: by_contra hni
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
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₂
⊢ i ∈ fs₁
have h₃ : ∀ (hni : i ∉ fs₁), False
Tactic: by_contra hni
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
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 univ (s.face h₁).points = Finset.centroid k univ (s.face h₂).points ↔ fs₁ = fs₂
have rw : Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂
Tactic: rw [face_centroid_eq_centroid, face_centroid_eq_centroid]
-- 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 : ℕ
s₁ s₂ : Simplex k P n
h : Set.range s₁.points = Set.range s₂.points
⊢ Finset.centroid k univ s₁.points = Finset.centroid k univ s₂.points
have h₁ : 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
Cleared hypotheses: h
-- 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 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ AffineIndependent k (Function.update (β := fun (a : Fin (n + 1)) ↦ P) s.points i s.centroid)
have this : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ (s.map f hf).centroid = (f : (a : P) → P₂) s.centroid
have 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₂)
Tactic: rw [centroid, map_points, centroid_eq_affineCombination, Finset.map_affineCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
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₂)
⊢ (s.map f hf).centroid = (f : (a : P) → P₂) s.centroid
have hw : Finset.sum (ι := Fin (n + 1)) univ (centroidWeights k univ) = 1
Tactic: rw [centroid, map_points, centroid_eq_affineCombination, Finset.map_affineCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → 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₂)
have 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₂)
Tactic: rw [Finset.centroid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ Finset.sum (ι := Fin (n + 1)) univ (centroidWeights k univ) = 1
have hw : card (α := Fin (n + 1)) univ ≠ 0
Tactic: rw [sum_centroidWeights_eq_one_of_card_ne_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Finset.centroid k univ (s.reindex e).points = Finset.centroid k univ s.points
have 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)
Tactic: simp only [centroid_eq_affineCombination]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ 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)
have 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)
Tactic: simp only [reindex]
-- 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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ 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)
have h_eq : m = n
Tactic: have h_eq : m = n := by simpa using Fintype.card_eq.2 ⟨e⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
h_eq : m = n
⊢ 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)
have 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)
Tactic: subst h_eq
Cleared hypotheses: n, e, h_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m : ℕ
s : Simplex k P m
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)
have h : univ = Finset.map e.toEmbedding univ
Tactic: convert! Finset.univ.affineCombination_map e.toEmbedding _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (m + 1)
h : univ = Finset.map e.toEmbedding univ
⊢ 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)
have 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))
Tactic: convert! Finset.univ.affineCombination_map e.toEmbedding _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ (↑(s.restrict S hS).centroid : P) = s.centroid
have rw : s.centroid = (↑(s.restrict S hS).centroid : P)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ s.centroid = (↑(s.restrict S hS).centroid : P)
have this : Nonempty.{u_3 + 1} ↥S
Tactic: haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
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
⊢ s.centroid = (↑(s.restrict S hS).centroid : P)
have hf : Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)
Tactic: have hf : Function.Injective (S.subtype) := by
    simp only [coe_subtype, Subtype.val_injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
have unfold : (s.faceOpposite i).centroid =
  (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
Tactic: unfold faceOppositeCentroid
-- 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
s : Simplex k P n
i : Fin (n + 1)
⊢ (s.faceOpposite i).centroid =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
have this : s.faceOpposite i = s.face (fs := {i}ᶜ) sorry
Tactic: have : s.faceOpposite i = s.face (fs := {i}ᶜ) (by simp [card_compl, NeZero.one_le]) := by rfl
-- 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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
⊢ (s.faceOpposite i).centroid =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
have rw : (s.face (fs := {i}ᶜ) sorry).centroid =
  (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
Tactic: rw [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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
⊢ Finset.centroid k univ (s.face (fs := {i}ᶜ) ⋯).points =
    (affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹
have rw : Eq.{u_3 + 1} (α := P)
  ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P)
      (Function.const (Fin (n + 1)) (↑(Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i}) : k)⁻¹) :
    P)
  ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)
Tactic: rw [face_centroid_eq_centroid, centroid_def, centroidWeights_eq_const, card_compl]
-- 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
s : Simplex k P n
i : Fin (n + 1)
this : s.faceOpposite i = s.face (fs := {i}ᶜ) ⋯
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P)
        (Function.const (Fin (n + 1)) (↑(Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i}) : k)⁻¹) :
      P)
    ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)
have simp : Eq.{u_3 + 1} (α := P)
  ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) (Function.const (Fin (n + 1)) (↑n : k)⁻¹) : P)
  ((affineCombination k {i}ᶜ s.points : (a : Fin (n + 1) → k) → P) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ : P)
Tactic: simp only [Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((weightedVSubOfPoint {i}ᶜ s.points (s.points i) : (a : Fin (n + 1) → k) → V) fun (x : Fin (n + 1)) ↦ (↑n : k)⁻¹ :
        V)
      (s.points i) -ᵥ
    s.points i =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (β := V) (↑n : k)⁻¹ (∑ x : Fin (n + 1), (s.points x -ᵥ s.points i))
Tactic: rw [faceOppositeCentroid_eq_affineCombination,
    affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ ?_ (s.points i)]