awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
hcard : #s' = n
hcard' : ∃ (a : Fin (n + 1)) (b : Fin (n + 1)), a ∈ s' ∧ b ∈ s' ∧ a ≠ b
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
h₁ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
w : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₂ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
w₁ : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have h₃ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s'
Tactic: tauto
Cleared hypotheses: hcard'
-- 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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
hcard : #s' = n
hcard' : ∃ (a : Fin (n + 1)) (b : Fin (n + 1)), a ∈ s' ∧ b ∈ s' ∧ a ≠ b
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
h₁ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
w : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₂ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
w₁ : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₃ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s'
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have h₄ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ¬w = a
Tactic: tauto
Cleared hypotheses: hcard'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
⊢ p -ᵥ s.centroid = 0
have he : ∃ (i : ↥s') (j : ↥s'), i ≠ j
Tactic: have he : ∃ i j : s', i ≠ j := by
    simp only [ne_eq, Subtype.exists, Subtype.mk.injEq, exists_prop]
    have hcard : s'.card = n := by
      rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
    have hcard' : 1 < #s' := by grind
    rw [Finset.one_lt_card_iff] at hcard'
    tauto
-- 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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
he : ∃ (i : ↥s') (j : ↥s'), i ≠ j
⊢ p -ᵥ s.centroid = 0
have choose : ∀ (i j : ↥s') (hij : i ≠ j), p -ᵥ s.centroid = 0
Tactic: choose i j hij using he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
⊢ p -ᵥ s.centroid = 0
have h_ij : Disjoint (α := Set ↥s') {i} {j}
Tactic: have h_ij : Disjoint ({i} : Set {x // x ∈ s'}) {j} := by simp [hij]
-- 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
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint (α := Set ↥s') {i} {j}
⊢ Disjoint (α := Submodule k V) (k ∙ u i) (k ∙ u j)
have simp_rw : Disjoint (α := Submodule k V) (Submodule.span k (u '' {i})) (Submodule.span k (u '' {j}))
Tactic: simp_rw [← Set.image_singleton, hi.disjoint_span_image h_ij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint (α := Set ↥s') {i} {j}
⊢ p -ᵥ s.centroid = 0
have h_disjoint : Disjoint (α := Submodule k V) (k ∙ u i) (k ∙ u j)
Tactic: have h_disjoint : Disjoint (Submodule.span k {u i}) (Submodule.span k {u j}) := by
    simp_rw [← Set.image_singleton, hi.disjoint_span_image h_ij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
⊢ AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (i : Fin (n + 1)) ↦ s.faceOppositeCentroid i
have h : AffineIndependent k s.points
Tactic: obtain h := s.independent
-- 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
h : AffineIndependent k s.points
⊢ AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (i : Fin (n + 1)) ↦ s.faceOppositeCentroid i
have rw : ∀
  (h :
    LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
      s.points (↑i : Fin (n + 1)) -ᵥ s.points 0),
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.faceOppositeCentroid (↑i : Fin (n + 1)) -ᵥ s.faceOppositeCentroid 0
Tactic: rw [affineIndependent_iff_linearIndependent_vsub k _ 0] at h ⊢
Cleared hypotheses: 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
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
h :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.points (↑i : Fin (n + 1)) -ᵥ s.points 0
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.faceOppositeCentroid (↑i : Fin (n + 1)) -ᵥ s.faceOppositeCentroid 0
have simp_rw : LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1)))
Tactic: simp_rw [faceOppositeCentroid_vsub_faceOppositeCentroid]
-- 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
h :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.points (↑i : Fin (n + 1)) -ᵥ s.points 0
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1)))
have h₁ : ∀ (i : { x : Fin (n + 1) // x ≠ 0 }),
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1))) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := { x : Fin (n + 1) // x ≠ 0 } → kˣ) (β := { x : Fin (n + 1) // x ≠ 0 } → V)
      (fun (x : { x : Fin (n + 1) // x ≠ 0 }) ↦ Units.mk0 (-(↑n : k))⁻¹ sorry)
      (fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.points 0) i
Tactic: convert! h.units_smul fun _ ↦ Units.mk0 (-n)⁻¹ (by simpa using NeZero.ne n) with i
-- 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 : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
inst_6 : CharZero k
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).medial = s.medial.reindex e
have h : ∀ (i : Fin (m + 1)), (s.reindex e).medial.points i = (s.medial.reindex e).points i
Tactic: ext i
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : CharZero k
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₂)
⊢ (s.map f hf).medial = s.medial.map f hf
have h : ∀ (i : Fin (n + 1)), (s.map f hf).medial.points i = (s.medial.map f hf).points i
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
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (affineSpan k (Set.range s.points))
have hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
Tactic: have hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points) :=
    mem_affineSpan _ (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
have apply : (↑(affineSpan k (Set.range (s.faceOpposite 0).points)) : Set P) ⊆ (↑(affineSpan k (Set.range s.points)) : Set P)
Tactic: apply Set.mem_of_mem_of_subset (s.faceOppositeCentroid_mem_affineSpan_face 0)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (affineSpan k (Set.range s.points))
have hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
Tactic: have hmem2 : s.medial.points 0 ∈ affineSpan k (Set.range s.points) := by
    apply Set.mem_of_mem_of_subset (s.faceOppositeCentroid_mem_affineSpan_face 0)
    exact affineSpan_mono k (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (affineSpan k (Set.range s.points))
have rw : Eq (α := Submodule k V) (direction (affineSpan k (Set.range s.medial.points)))
  (direction (affineSpan k (Set.range s.points)))
Tactic: rw [eq_iff_direction_eq_of_mem hmem1 hmem2]
-- 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
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
⊢ Eq (α := Submodule k V) (direction (affineSpan k (Set.range s.medial.points)))
    (direction (affineSpan k (Set.range s.points)))
have simp_rw : Eq (α := Submodule k V) (Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points))
  (Submodule.span k (Set.range s.points -ᵥ Set.range s.points))
Tactic: simp_rw [direction_affineSpan, vectorSpan_def]
-- 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
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
this :
  Set.range s.medial.points -ᵥ Set.range s.medial.points =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
⊢ Eq (α := Submodule k V) (Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points))
    (Submodule.span k (Set.range s.points -ᵥ Set.range s.points))
have hr : IsUnit.{u_1} (M := k) (-(↑n : k))⁻¹
Tactic: rw [this, Submodule.span_smul_eq_of_isUnit]
-- 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
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
⊢ Eq (α := Submodule k V) (Submodule.span k (Set.range s.medial.points -ᵥ Set.range s.medial.points))
    (Submodule.span k (Set.range s.points -ᵥ Set.range s.points))
have suffices : Set.range s.medial.points -ᵥ Set.range s.medial.points =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
Tactic: suffices Set.range s.medial.points -ᵥ Set.range s.medial.points
    = (-n : k)⁻¹ • (Set.range s.points -ᵥ Set.range s.points) by
    rw [this, Submodule.span_smul_eq_of_isUnit]
    simpa using NeZero.ne n
-- 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
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
⊢ Set.range s.medial.points -ᵥ Set.range s.medial.points =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
have h : ∀ (v : V),
  v ∈ Set.range s.medial.points -ᵥ Set.range s.medial.points ↔
    v ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
Tactic: ext v
-- 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
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
v : V
⊢ v ∈ Set.range s.medial.points -ᵥ Set.range s.medial.points ↔
    v ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k))⁻¹ (Set.range s.points -ᵥ Set.range s.points)
have h : (∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) = v) ↔
  ∃ (a : Fin (n + 1)) (b : Fin (n + 1)), -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b) = v
Tactic: suffices (∃ a b, (n : k)⁻¹ • (s.points b -ᵥ s.points a) = v) ↔
    ∃ a b, -((n : k)⁻¹ • (s.points a -ᵥ s.points b)) = v by
    simpa [Set.mem_vsub, Set.mem_smul_set, medial_points,
      faceOppositeCentroid_vsub_faceOppositeCentroid]
-- 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
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
hmem2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)
v : V
⊢ (∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) = v) ↔
    ∃ (a : Fin (n + 1)) (b : Fin (n + 1)),
      -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b) = v
have h : ∀ (a b : Fin (n + 1)),
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points b -ᵥ s.points a) =
    -HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points a -ᵥ s.points b)
Tactic: congrm ∃ a b, ?_ = v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ (s.restrict S hS).medial = s.medial.restrict S ⋯
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 (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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_3 + 1} ↥S
⊢ (s.restrict S hS).medial = s.medial.restrict S ⋯
have h : ∀ (i : Fin (n + 1)),
  (↑((s.restrict S hS).medial.points i) : P) = (↑(points (s.medial.restrict S sorry : Simplex k (↥S) n) i) : P)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
⊢ slope f a a = 0
have rw : (a - a)⁻¹ • (f a -ᵥ f a) = 0
Tactic: rw [slope, sub_self, inv_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
rw : (a - a)⁻¹ • (f a -ᵥ f a) = 0
⊢ slope f a a = 0
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0⁻¹ (f a -ᵥ f a) = 0
Tactic: rw [slope, sub_self, inv_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
rw : (a - a)⁻¹ • (f a -ᵥ f a) = 0
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0⁻¹ (f a -ᵥ f a) = 0
⊢ slope f a a = 0
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (f a -ᵥ f a) = 0
Tactic: rw [slope, sub_self, inv_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
rw : (a - a)⁻¹ • (f a -ᵥ f a) = 0
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0⁻¹ (f a -ᵥ f a) = 0
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (f a -ᵥ f a) = 0
⊢ slope f a a = 0
have rw₃ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [slope, sub_self, inv_zero, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b = f b -ᵥ f a
have inl : (a - a) • slope f a a = f a -ᵥ f a
Tactic: rcases eq_or_ne a b with (rfl | hne)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b : k
inl : (a - a) • slope f a a = f a -ᵥ f a
⊢ (b - a) • slope f a b = f b -ᵥ f a
have inr : ∀ (hne : a ≠ b), (b - a) • slope f a b = f b -ᵥ f a
Tactic: rcases eq_or_ne a b with (rfl | hne)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a : k
⊢ (a - a) • slope f a a = f a -ᵥ f a
have inl : HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 (slope f a a) = f a -ᵥ f a
Tactic: rw [sub_self, zero_smul, vsub_self]